:: Implicit Function Theorem -- Part {I}
:: by Kazuhisa Nakasho , Yuichi Futa and Yasunari Shidama
::
:: Received November 29, 2017
:: Copyright (c) 2017-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, REAL_1, ZFMISC_1, NORMSP_1, PRE_TOPC, PARTFUN1, FUNCT_1,
NAT_1, FDIFF_1, SUBSET_1, XXREAL_1, FINSEQ_2, RELAT_1, LOPBAN_1, RCOMP_1,
MSSUBFAM, SQUARE_1, TARSKI, ARYTM_3, VALUED_1, FUNCT_2, ARYTM_1, SEQ_2,
ORDINAL2, SUPINF_2, FCONT_1, STRUCT_0, CARD_1, XXREAL_0, XBOOLE_0,
FINSEQ_1, RLVECT_1, CFCONT_1, NDIFF_7, MCART_1, NORMSP_2, METRIC_1,
POWER, COMPLEX1, LOPBAN_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
RELSET_1,
PARTFUN1, FUNCT_2, BINOP_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0,
SQUARE_1, NAT_1, COMPLEX1, FINSEQ_1, FINSEQ_2, VALUED_1, SEQ_2, POWER,
STRUCT_0, PRE_TOPC, RLVECT_1, VECTSP_1, NORMSP_0, NORMSP_1, VFUNCT_1,
EUCLID, LOPBAN_1, LOPBAN_2, NFCONT_1, LOPBAN_5, NDIFF_1, NDIFF_2,
NORMSP_2, PRVECT_3, NDIFF_5, NDIFF_7;
constructors SQUARE_1, SEQ_2, NFCONT_1, VFUNCT_1, COMSEQ_2, NDIFF_1, RELSET_1,
NAT_D, SERIES_1, RSSPACE3, LOPBAN_3, NDIFF_5, NDIFF_2, DOMAIN_1,
LOPBAN_5, PCOMPS_1, NDIFF_7, NORMSP_2;
registrations RELSET_1, STRUCT_0, XREAL_0, MEMBERED, FUNCT_1, VALUED_0,
VALUED_1, FINSEQ_2, FUNCT_2, NUMBERS, XBOOLE_0, RELAT_1, ORDINAL1,
LOPBAN_1, PRVECT_3, NORMSP_0, NAT_1, NORMSP_1, SQUARE_1, XTUPLE_0;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TARSKI;
equalities RLVECT_1, LOPBAN_1, NDIFF_2, NORMSP_0, BINOP_1, EUCLID, SQUARE_1,
NORMSP_2, LOPBAN_5, FINSEQ_2, NDIFF_5, LOPBAN_2, PCOMPS_1;
expansions VECTSP_1, NDIFF_7;
theorems TARSKI, XBOOLE_0, XBOOLE_1, RLVECT_1, ZFMISC_1, RELAT_1, FUNCT_1,
SQUARE_1, VFUNCT_1, FUNCT_2, FINSEQ_1, LOPBAN_1, PARTFUN1, NFCONT_1,
NDIFF_1, VECTSP_1, SEQ_2, COMPLEX1, POWER, XXREAL_0, NAT_1, XCMPLX_1,
RLTOPSP1, ABSVALUE, NORMSP_0, NDIFF_2, PRVECT_3, NDIFF_5, SEQ_1,
RSSPACE3, LOPBAN_3, RLVECT_4, NORMSP_2, NDIFF_7, XTUPLE_0, NORMSP_1,
TOPS_2, RELSET_1, EUCLID_3, XREAL_1, LOPBAN_2, LOPBAN_7, NFCONT_2;
schemes FUNCT_1, FUNCT_2, FRAENKEL, NAT_1;
begin :: 1. Properties of Lipschitz continuous linear function
reserve S,T,W,Y for RealNormSpace;
reserve f,f1,f2 for PartFunc of S,T;
reserve Z for Subset of S;
reserve i,n for Nat;
theorem LMNR0:
for X,Y be RealNormSpace,
x be Point of X,
y be Point of Y,
z be Point of [:X,Y:]
st z = [x,y]
holds ||.z.|| = sqrt (||.x.|| ^2 + ||.y.|| ^2)
proof
let X,Y be RealNormSpace,
x be Point of X,
y be Point of Y,
z be Point of [:X,Y:];
assume z = [x,y]; then
consider w be Element of REAL 2 such that
A1: w = <* ||.x.||,||.y.|| *> & ||.z.|| = |.w.| by PRVECT_3:18;
w in 2 -tuples_on REAL; then
A2: ex s be Element of REAL* st s = w & len s = 2;
w . 1 = ||.x.|| & w . 2 = ||.y.|| by A1,FINSEQ_1:44;
hence thesis by A1,A2,EUCLID_3:22;
end;
theorem LMNR1:
for X,Y be RealNormSpace,
x be Point of X,
z be Point of [:X,Y:]
st z = [x,0.Y]
holds ||.z.|| = ||.x.||
proof
let X,Y be RealNormSpace,
x be Point of X,
z be Point of [:X,Y:];
assume z = [x,0.Y]; then
||.z.|| = sqrt (||.x.|| ^2 + ||.0.Y.|| ^2) by LMNR0
.= sqrt (||.x.|| ^2);
hence ||.x.|| = ||.z.|| by SQUARE_1:22;
end;
theorem
for X,Y be RealNormSpace,
y be Point of Y,
z be Point of [:X,Y:]
st z = [0.X,y]
holds ||.z.|| = ||.y.||
proof
let X,Y be RealNormSpace,
y be Point of Y,
z be Point of [:X,Y:];
assume z = [0.X,y]; then
||.z.|| = sqrt(||.0.X.|| ^2 + ||.y.|| ^2) by LMNR0
.= sqrt(||.y.|| ^2);
hence ||.y.|| = ||.z.|| by SQUARE_1:22;
end;
theorem
for X,Y,Z,W be RealNormSpace
for f be Lipschitzian LinearOperator of Z,W,
g be Lipschitzian LinearOperator of Y,Z,
h be Lipschitzian LinearOperator of X,Y
holds f*(g*h) = (f*g)*h by RELAT_1:36;
theorem LPB2Th4:
for X,Y,Z be RealNormSpace
for g be Lipschitzian LinearOperator of X,Y,
f be Lipschitzian LinearOperator of Y,Z,
h be Lipschitzian LinearOperator of X,Z
holds h = f*g iff for x be VECTOR of X holds h.x = f.(g.x)
proof
let X,Y,Z be RealNormSpace;
let g be Lipschitzian LinearOperator of X,Y,
f be Lipschitzian LinearOperator of Y,Z,
h be Lipschitzian LinearOperator of X,Z;
now
assume
A1: for x being VECTOR of X holds h.x = f.(g.x);
now
let x be VECTOR of X;
thus (f*g).x = f.(g.x) by FUNCT_2:15
.= h.x by A1;
end;
hence h = f*g by FUNCT_2:63;
end;
hence thesis by FUNCT_2:15;
end;
theorem LPB2Th6:
for X,Y be RealNormSpace for f be Lipschitzian LinearOperator of X,Y
holds f * (id the carrier of X) = f & (id the carrier of Y) * f = f
proof
let X,Y be RealNormSpace;
reconsider ii = id the carrier of X
as Lipschitzian LinearOperator of X,X by LOPBAN_2:3;
reconsider jj = id the carrier of Y
as Lipschitzian LinearOperator of Y,Y by LOPBAN_2:3;
let f be Lipschitzian LinearOperator of X,Y;
A1: now
let x be VECTOR of X;
thus ((id the carrier of Y)*f).x = jj.(f.x) by FUNCT_2:15
.= f.x;
end;
now
let x be VECTOR of X;
thus (f*(id the carrier of X)).x = f.(ii.x) by FUNCT_2:15
.= f.x;
end;
hence thesis by A1,FUNCT_2:63;
end;
theorem
for X,Y,Z,W be RealNormSpace
for f be Element of BoundedLinearOperators(Z,W),
g be Element of BoundedLinearOperators(Y,Z),
h be Element of BoundedLinearOperators(X,Y)
holds f*(g*h) = (f*g)*h
proof
let X,Y,Z,W be RealNormSpace;
let f be Element of BoundedLinearOperators(Z,W),
g be Element of BoundedLinearOperators(Y,Z),
h be Element of BoundedLinearOperators(X,Y);
modetrans((g*h),X,Z)
= modetrans(g,Y,Z) * modetrans(h,X,Y) by LOPBAN_1:def 11; then
modetrans(f,Z,W) * modetrans((g*h),X,Z)
= (modetrans(f,Z,W) * modetrans(g,Y,Z)) * modetrans(h,X,Y)
by RELAT_1:36;
hence thesis by LOPBAN_1:def 11;
end;
theorem
for X,Y be RealNormSpace for f be Element of BoundedLinearOperators
(X,Y) holds f * FuncUnit(X) = f & FuncUnit(Y) * f = f
proof
let X,Y be RealNormSpace;
let f be Element of BoundedLinearOperators(X,Y);
(id the carrier of X) is Lipschitzian LinearOperator of X,X
by LOPBAN_2:3; then
(id the carrier of X) is Element of BoundedLinearOperators(X,X)
by LOPBAN_1:def 9; then
modetrans((id(the carrier of X)),X,X)
= (id the carrier of X) by LOPBAN_1:def 11;
hence f * FuncUnit(X) = modetrans(f,X,Y) by LPB2Th6
.= f by LOPBAN_1:def 11;
(id the carrier of Y) is Lipschitzian LinearOperator of Y,Y
by LOPBAN_2:3; then
(id the carrier of Y) is Element of BoundedLinearOperators(Y,Y)
by LOPBAN_1:def 9; then
modetrans( (id (the carrier of Y)),Y,Y)
= (id the carrier of Y) by LOPBAN_1:def 11;
hence FuncUnit(Y) * f = modetrans(f,X,Y) by LPB2Th6
.= f by LOPBAN_1:def 11;
end;
theorem LPB2Th9:
for X,Y,Z be RealNormSpace
for f be Element of R_NormSpace_of_BoundedLinearOperators(Y,Z),
g,h be Element of R_NormSpace_of_BoundedLinearOperators(X,Y)
holds f * (g + h) = f*g + f*h
proof
let X,Y,Z be RealNormSpace;
let f be Element of R_NormSpace_of_BoundedLinearOperators(Y,Z),
g,h be Element of R_NormSpace_of_BoundedLinearOperators(X,Y);
set BLOPXY = R_NormSpace_of_BoundedLinearOperators(X,Y);
set BLOPXZ = R_NormSpace_of_BoundedLinearOperators(X,Z);
set mf = modetrans(f,Y,Z);
set mg = modetrans(g,X,Y);
set mh = modetrans(h,X,Y);
set mgh= modetrans(g+h, X,Y);
A1: mf*mh is Lipschitzian LinearOperator of X,Z by LOPBAN_2:2; then
reconsider fh=mf*mh as VECTOR of BLOPXZ by LOPBAN_1:def 9;
A2: mf*mg is Lipschitzian LinearOperator of X,Z by LOPBAN_2:2; then
reconsider fg=mf*mg as VECTOR of BLOPXZ by LOPBAN_1:def 9;
A3: mf*mgh is Lipschitzian LinearOperator of X,Z by LOPBAN_2:2; then
reconsider k=mf*mgh as VECTOR of BLOPXZ by LOPBAN_1:def 9;
reconsider hh = h as VECTOR of BLOPXY;
reconsider gg = g as VECTOR of BLOPXY;
A4: gg = mg & hh = mh by LOPBAN_1:def 11;
for x be VECTOR of X holds (mf*mgh).x=(mf*mg).x + (mf*mh).x
proof
let x be VECTOR of X;
g+h=gg+hh & modetrans(g+h, X,Y) =g+h by LOPBAN_1:def 11; then
A5: mgh.x=mg.x+mh.x by A4,LOPBAN_1:35;
thus (mf*mgh).x = mf.(mgh.x) by A3,LPB2Th4
.= mf.(mg.x) + mf.(mh.x) by A5,VECTSP_1:def 20
.= (mf*mg).x + mf.(mh.x) by A2,LPB2Th4
.= (mf*mg).x + (mf*mh).x by A1,LPB2Th4;
end;
hence thesis by LOPBAN_1:35;
end;
theorem
for X,Y,Z be RealNormSpace
for f be Element of R_NormSpace_of_BoundedLinearOperators(X,Y),
g,h be Element of R_NormSpace_of_BoundedLinearOperators(Y,Z)
holds (g + h) * f = g*f + h*f
proof
let X,Y,Z be RealNormSpace;
let f be Element of R_NormSpace_of_BoundedLinearOperators(X,Y),
g,h be Element of R_NormSpace_of_BoundedLinearOperators(Y,Z);
set BLOPXY = R_NormSpace_of_BoundedLinearOperators(X,Y);
set BLOPXZ = R_NormSpace_of_BoundedLinearOperators(X,Z);
set BLOPYZ = R_NormSpace_of_BoundedLinearOperators(Y,Z);
set mf = modetrans(f,X,Y);
set mg = modetrans(g,Y,Z);
set mh = modetrans(h,Y,Z);
set mgh= modetrans(g+h, Y,Z);
A1: mh*mf is Lipschitzian LinearOperator of X,Z by LOPBAN_2:2; then
reconsider hf = mh*mf as VECTOR of BLOPXZ by LOPBAN_1:def 9;
A2: mg*mf is Lipschitzian LinearOperator of X,Z by LOPBAN_2:2; then
reconsider gf=mg*mf as VECTOR of BLOPXZ by LOPBAN_1:def 9;
A3: mgh*mf is Lipschitzian LinearOperator of X,Z by LOPBAN_2:2; then
reconsider k = mgh*mf as VECTOR of BLOPXZ by LOPBAN_1:def 9;
reconsider hh = h as VECTOR of BLOPYZ;
reconsider gg = g as VECTOR of BLOPYZ;
A4: gg = mg & hh = mh by LOPBAN_1:def 11;
for x be VECTOR of X holds (mgh*mf).x=(mg*mf).x + (mh*mf).x
proof
let x be VECTOR of X;
g+h = gg+hh & modetrans(g+h, Y,Z) = g+h by LOPBAN_1:def 11; then
A5: mgh.(mf.x) = mg.(mf.x) + mh.(mf.x) by A4,LOPBAN_1:35;
thus (mgh*mf).x = mgh.(mf.x) by A3,LPB2Th4
.= (mg*mf).x + mh.(mf.x) by A2,A5,LPB2Th4
.= (mg*mf).x + (mh*mf).x by A1,LPB2Th4;
end;
hence thesis by LOPBAN_1:35;
end;
theorem LPB2Th11:
for X,Y,Z be RealNormSpace
for f be Element of R_NormSpace_of_BoundedLinearOperators(Y,Z),
g be Element of R_NormSpace_of_BoundedLinearOperators(X,Y)
for a,b be Real holds (a*b) * (f*g) = (a*f) * (b*g)
proof
let X,Y,Z be RealNormSpace;
let f be Element of R_NormSpace_of_BoundedLinearOperators(Y,Z),
g be Element of R_NormSpace_of_BoundedLinearOperators(X,Y);
let a,b be Real;
set BLOPXY=R_NormSpace_of_BoundedLinearOperators(X,Y);
set BLOPXZ=R_NormSpace_of_BoundedLinearOperators(X,Z);
set BLOPYZ=R_NormSpace_of_BoundedLinearOperators(Y,Z);
set mf = modetrans(f,Y,Z);
set mg = modetrans(g,X,Y);
set maf= modetrans((a*f),Y,Z);
set mbg= modetrans(b*g,X,Y);
A1: maf*mbg is Lipschitzian LinearOperator of X,Z by LOPBAN_2:2; then
reconsider k=(maf)*(mbg) as VECTOR of BLOPXZ by LOPBAN_1:def 9;
A2: mf*mg is Lipschitzian LinearOperator of X,Z by LOPBAN_2:2; then
reconsider fg = mf*mg as VECTOR of BLOPXZ by LOPBAN_1:def 9;
reconsider ff = f as VECTOR of BLOPYZ;
reconsider gg = g as VECTOR of BLOPXY;
A3: gg = mg by LOPBAN_1:def 11;
A4: ff = mf by LOPBAN_1:def 11;
for x be VECTOR of X holds ( (maf)*(mbg)).x=(a*b)*(mf*mg).x
proof
let x be VECTOR of X;
set y = b*mg.x;
a*f = a*ff & modetrans(a*f, Y,Z) = a*f by LOPBAN_1:def 11; then
A5: maf.y = a*mf.y by A4,LOPBAN_1:36;
b*g = b*gg & modetrans(b*g, X,Y) = b*g by LOPBAN_1:def 11; then
A6: mbg.x = b*mg.x by A3,LOPBAN_1:36;
thus (maf*mbg).x = maf.(mbg.x) by A1,LPB2Th4
.= a * (b*mf.(mg.x)) by A5,A6,LOPBAN_1:def 5
.= (a*b) * mf.(mg.x) by RLVECT_1:def 7
.= (a*b) * (mf*mg).x by A2,LPB2Th4;
end;
hence thesis by LOPBAN_1:36;
end;
theorem
for X,Y,Z be RealNormSpace
for f be Element of R_NormSpace_of_BoundedLinearOperators(Y,Z),
g be Element of R_NormSpace_of_BoundedLinearOperators(X,Y)
for a be Real
holds a*(f*g) = (a*f)*g
proof
let X,Y,Z be RealNormSpace;
let f be Element of R_NormSpace_of_BoundedLinearOperators(Y,Z),
g be Element of R_NormSpace_of_BoundedLinearOperators(X,Y);
let a be Real;
reconsider jj = 1 as Real;
a*(f*g) = (a*jj) * (f*g)
.= (a*f) * (jj*g) by LPB2Th11;
hence thesis by RLVECT_1:def 8;
end;
begin :: 2. Properties of open and closed sets in Banach space
definition
let M be RealNormSpace, p be Element of M, r be Real;
func cl_Ball(p,r) -> Subset of M equals
{q where q is Element of M : ||.p - q.|| <= r};
correctness
proof
defpred P[Element of M] means ||.p - $1.|| <= r;
set X = {q where q is Element of M: P[q]};
X c= the carrier of M from FRAENKEL:sch 10;
hence thesis;
end;
end;
theorem LMBALL2:
for p be Element of S, r be Real st 0 < r holds
p in Ball(p,r) & p in cl_Ball(p,r)
proof
let p be Element of S, r be Real;
assume
A1: 0 < r;
A2: ||. p - p .|| = ||. 0.S .|| by RLVECT_1:15
.= 0;
hence p in Ball(p,r) by A1;
thus p in cl_Ball(p,r) by A1,A2;
end;
theorem
for p be Element of S, r be Real st 0 < r holds
Ball(p,r) <> {} & cl_Ball(p,r) <> {} by LMBALL2;
theorem LMBALL1:
for M be RealNormSpace, p be Element of M, r1,r2 be Real
st r1 <= r2 holds
cl_Ball(p,r1) c= cl_Ball(p,r2)
& Ball(p,r1) c= cl_Ball(p,r2)
& Ball(p,r1) c= Ball(p,r2)
proof
let M be RealNormSpace, p be Element of M,
r1,r2 be Real;
assume
A1: r1 <= r2;
thus cl_Ball(p,r1) c= cl_Ball(p,r2)
proof
let x be object;
assume
A2: x in cl_Ball(p,r1); then
reconsider y=x as Point of M;
ex q be Element of M st y=q & ||.p - q.|| <= r1 by A2; then
||.p - y.|| <= r2 by A1,XXREAL_0:2;
hence x in cl_Ball(p,r2);
end;
thus Ball(p,r1) c= cl_Ball(p,r2)
proof
let x be object;
assume
A3: x in Ball(p,r1); then
reconsider y = x as Point of M;
ex q be Element of M st y = q & ||.p - q.|| < r1 by A3; then
||.p - y.|| <= r2 by A1,XXREAL_0:2;
hence x in cl_Ball(p,r2);
end;
let x be object;
assume
A4: x in Ball(p,r1); then
reconsider y = x as Point of M;
ex q be Element of M st y = q & ||.p - q.|| < r1 by A4; then
||.p - y.|| < r2 by A1,XXREAL_0:2;
hence x in Ball(p,r2);
end;
theorem LMBALL1X:
for M be RealNormSpace, p be Element of M, r1,r2 be Real
st r1 < r2 holds
cl_Ball(p,r1) c= Ball(p,r2)
proof
let M be RealNormSpace,
p be Element of M, r1,r2 be Real;
assume
A1: r1 < r2;
assume not cl_Ball(p,r1) c= Ball(p,r2); then
consider x be object such that
A2: x in cl_Ball(p,r1) & not x in Ball(p,r2) by TARSKI:def 3;
reconsider x as Point of M by A2;
A3: ex q be Element of M st x = q & ||.p - q.|| <= r1 by A2;
r2 <= ||.p - x.|| by A2;
hence contradiction by A1,A3,XXREAL_0:2;
end;
theorem LMBALL:
for p be Element of S, r be Real holds
Ball(p,r) = {y where y is Point of S: ||.y - p.|| < r}
proof
let p be Element of S,r be Real;
deffunc F(object) = $1;
defpred P1[Element of S] means ||.p - $1.|| < r;
defpred P2[Element of S] means ||.$1 - p.|| < r;
A1: for v being Element of the carrier of S holds
(P1[v] iff P2[v]) by NORMSP_1:7;
{F(y) where y is Element of the carrier of S: P1[y]}
= {F(y) where y is Element of the carrier of S: P2[y]}
from FRAENKEL:sch 3(A1);
hence thesis;
end;
theorem
for p be Element of S, r be Real holds
cl_Ball(p,r) = {y where y is Point of S: ||.y - p.|| <= r}
proof
let p be Element of S,r be Real;
deffunc F(object) = $1;
defpred P1[Element of S] means ||.p - $1.||<=r;
defpred P2[Element of S] means ||.$1 - p.||<=r;
A1: for v being Element of the carrier of S holds
(P1[v] iff P2[v]) by NORMSP_1:7;
{F(y) where y is Element of the carrier of S: P1[y]}
= {F(y) where y is Element of the carrier of S: P2[y]}
from FRAENKEL:sch 3(A1);
hence thesis;
end;
theorem
for p be Element of S, r be Real st 0 < r
holds Ball(p,r) is Neighbourhood of p
proof
let p be Element of S,r be Real;
assume 0 < r; then
{y where y is Point of S: ||.y - p.|| < r}
is Neighbourhood of p by NFCONT_1:3;
hence thesis by LMBALL;
end;
registration let X be RealNormSpace, x be Point of X, r be Real;
cluster Ball(x,r) -> open;
coherence
proof
defpred P[Element of X] means ||.x - $1.|| < r;
set K = {q where q is Point of X: P[q]};
K c= the carrier of X from FRAENKEL:sch 10; then
reconsider K as Subset of X;
reconsider T = K as Subset of TopSpaceNorm X;
T is open by NORMSP_2:8;
hence thesis by NORMSP_2:16;
end;
cluster cl_Ball(x,r) -> closed;
coherence
proof
defpred P[Element of X] means ||.x-$1.||<=r;
set K = {q where q is Point of X: P[q]};
K c= the carrier of X from FRAENKEL:sch 10; then
reconsider K as Subset of X;
reconsider T = K as Subset of TopSpaceNorm X;
T is closed by NORMSP_2:9;
hence thesis by NORMSP_2:15;
end;
end;
theorem NORMSP27:
for X be RealNormSpace, V be Subset of X holds V is open
iff for x be Point of X st x in V ex r be Real st r>0 & Ball(x,r) c= V
proof
let X be RealNormSpace, V be Subset of X;
reconsider V0 = V as Subset of TopSpaceNorm X;
hereby
assume V is open; then
A1: V0 is open by NORMSP_2:16;
thus for x be Point of X st x in V
ex r be Real st r>0 & Ball(x,r) c= V
proof
let x be Point of X;
assume x in V; then
consider r be Real such that
A2: r>0
& {y where y is Point of X: ||.x-y.|| < r} c= V0 by A1,NORMSP_2:7;
take r;
thus thesis by A2;
end;
end;
assume
A3: for x be Point of X st x in V
ex r be Real st r>0 & Ball(x,r) c= V;
for x be Point of X st x in V0
ex r be Real st r>0
& {y where y is Point of X: ||.x-y.|| < r} c= V0
proof
let x be Point of X;
assume x in V0; then
consider r be Real such that
A4: r>0 & Ball(x,r) c= V by A3;
take r;
thus thesis by A4;
end; then
V0 is open by NORMSP_2:7;
hence thesis by NORMSP_2:16;
end;
theorem NORMSP35:
for X,Y be RealNormSpace,
x be Point of X,
y be Point of Y,
z be Point of [:X,Y:]
st z = [x,y]
holds ||.x.|| <= ||.z.|| & ||.y.|| <= ||.z.||
proof
let X,Y be RealNormSpace,
x be Point of X,
y be Point of Y,
z be Point of [:X,Y:];
assume z = [x,y]; then
A2: ||.z.|| = sqrt(||.x.|| ^2 + ||.y.|| ^2) by LMNR0;
0 + ||.x.|| ^2 <= ||.x.|| ^2 + ||.y.|| ^2 by XREAL_1:6; then
sqrt(||.x.|| ^2) <= sqrt (||.x.|| ^2 + ||.y.|| ^2) by SQUARE_1:26;
hence ||.x.|| <= ||.z.|| by A2,SQUARE_1:22;
0 + ||.y.|| ^2 <= ||.x.|| ^2 + ||.y.|| ^2 by XREAL_1:6; then
sqrt(||.y.|| ^2) <= sqrt(||.x.|| ^2 + ||.y.|| ^2) by SQUARE_1:26;
hence ||.y.|| <= ||.z.|| by A2,SQUARE_1:22;
end;
theorem NORMSP31:
for X,Y be RealNormSpace,
x be Point of X,
y be Point of Y,
z be Point of [:X,Y:],
r1 be Real
st 0 < r1 & z = [x,y]
holds
ex r2 be Real
st 0 < r2 & r2 < r1 & [:Ball(x,r2),Ball(y,r2):] c= Ball(z,r1)
proof
let X,Y be RealNormSpace,
x be Point of X,
y be Point of Y,
z be Point of [:X,Y:],
r1 be Real;
assume
A1: 0 < r1 & z = [x,y];
take r2 = r1/2;
thus 0<r2 & r2<r1 by A1,XREAL_1:215,XREAL_1:216;
A2: r1^2 / 2 < r1^2 by A1,SQUARE_1:12,XREAL_1:216;
thus [:Ball(x,r2),Ball(y,r2):] c= Ball(z,r1)
proof
let w be object;
assume w in [:Ball(x,r2),Ball(y,r2):]; then
consider x1,y1 be object such that
A3: x1 in Ball(x,r2) & y1 in Ball(y,r2)
& w = [x1,y1] by ZFMISC_1:def 2;
reconsider x1 as Point of X by A3;
reconsider y1 as Point of Y by A3;
[x1,y1] is set; then
reconsider xy = w as Point of [:X,Y:] by A3;
ex p be Point of X st x1 = p & ||.x - p.|| < r2 by A3; then
A4: ||.x - x1.||^2 < r2 ^2 by SQUARE_1:16;
ex p be Point of Y st y1 = p & ||.y - p.|| < r2 by A3; then
A5: ||.y - y1.||^2 < r2 ^2 by SQUARE_1:16;
-xy = [-x1,-y1] by A3,PRVECT_3:18; then
z - xy = [x-x1, y-y1 ] by A1,PRVECT_3:18; then
A7: ||.z -xy.|| = sqrt (||.x-x1.|| ^2 + ||.y-y1.|| ^2) by LMNR0;
||.x-x1.|| ^2 + ||.y-y1.|| ^2 < r2^2 + r2^2 by A4,A5,XREAL_1:8; then
||.x-x1.|| ^2 + ||.y-y1.|| ^2 < r1^2 by A2,XXREAL_0:2; then
sqrt (||.x-x1.|| ^2 + ||.y-y1.|| ^2) < sqrt (r1^2) by SQUARE_1:27; then
||.z -xy.|| <r1 by A1,A7,SQUARE_1:22;
hence w in Ball(z,r1);
end;
end;
theorem
for X,Y be RealNormSpace,
x be Point of X,
y be Point of Y,
V be Subset of [:X,Y:]
st V is open & [x,y] in V
ex r be Real st 0 < r & [:Ball(x,r),Ball(y,r):] c= V
proof
let X,Y be RealNormSpace,
x be Point of X,
y be Point of Y,
V be Subset of [:X,Y:];
assume
A1: V is open & [x,y] in V;
reconsider z = [x,y] as Point of [:X,Y:];
consider r be Real such that
A2: r>0 & Ball(z,r) c= V by A1,NORMSP27;
consider r2 be Real such that
A3: 0 < r2 & r2 < r
& [:Ball(x,r2),Ball(y,r2):] c= Ball(z,r) by A2,NORMSP31;
take r2;
thus 0 < r2 by A3;
thus [:Ball(x,r2),Ball(y,r2):] c= V by A2,A3,XBOOLE_1:1;
end;
theorem
for X,Y be RealNormSpace,
x be Point of X,
y be Point of Y,
V be Subset of [:X,Y:],
r be Real
st V = [:Ball(x,r),Ball(y,r):]
holds V is open
proof
let X,Y be RealNormSpace,
x be Point of X,
y be Point of Y,
V be Subset of [:X,Y:],
r be Real;
assume
A1: V = [:Ball(x,r),Ball(y,r):];
for z be Point of [:X,Y:] st z in V
ex s be Real st s > 0 & Ball(z,s) c= V
proof
let z be Point of [:X,Y:];
assume
A2: z in V;
consider x1 be Point of X,y1 be Point of Y such that
A3: z = [x1,y1] by PRVECT_3:18;
A4: x1 in Ball(x,r) & y1 in Ball(y,r) by A1,A2,A3,ZFMISC_1:87;
A5: ex p be Point of X
st x1 = p & ||.x - p.|| < r by A4;
A6: ex p be Point of Y st y1 = p & ||.y - p.|| < r by A4;
set r1 = r - ||.x - x1.||;
set r2 = r - ||.y - y1.||;
A7: 0 < r1 by A5,XREAL_1:50;
A8: 0 < r2 by A6,XREAL_1:50;
reconsider s = min(r1,r2) as Real;
A9: 0 < s by A7,A8,XXREAL_0:15;
A10: s <= r - ||.x - x1.|| by XXREAL_0:17;
A11: s <= r - ||.y - y1.|| by XXREAL_0:17;
Ball(z,s) c= V
proof
let w be object;
assume
A12: w in Ball(z,s); then
reconsider q = w as Point of [:X,Y:];
A13: ex t be Point of [:X,Y:] st q = t & ||.z - t.|| < s by A12;
consider qx be Point of X,qy be Point of Y such that
A14: q = [qx,qy] by PRVECT_3:18;
-q = [-qx,-qy] by A14,PRVECT_3:18; then
z - q = [x1-qx, y1-qy] by A3,PRVECT_3:18; then
||.x1-qx .|| <= ||.z - q.||
& ||.y1-qy .|| <= ||.z - q.|| by NORMSP35; then
A16: ||.x1-qx .|| < s & ||.y1-qy .|| < s by A13,XXREAL_0:2;
(x-x1) + (x1-qx) = x-x1 + x1-qx by RLVECT_1:28
.= x-qx by RLVECT_4:1; then
A17: ||.x-qx.|| <= ||.x-x1.|| + ||.x1-qx.|| by NORMSP_1:def 1;
A18: ||.x-x1.|| + ||.x1-qx.|| < ||.x-x1.|| + s by A16,XREAL_1:8;
||.x-x1.|| + s <= ||.x-x1.|| + (r - ||.x - x1.||) by A10,XREAL_1:7;
then ||.x-x1.|| + ||.x1-qx.|| < r by A18,XXREAL_0:2; then
||.x-qx.|| < r by A17,XXREAL_0:2; then
A19: qx in Ball(x,r);
(y-y1) + (y1-qy) = y-y1 + y1-qy by RLVECT_1:28
.= y-qy by RLVECT_4:1; then
A20: ||.y-qy.|| <= ||.y-y1.|| + ||.y1-qy.|| by NORMSP_1:def 1;
A21: ||.y-y1.|| + ||.y1-qy.|| < ||.y-y1.|| + s by A16,XREAL_1:8;
||.y-y1.|| + s <= ||.y-y1.|| + (r - ||.y - y1.||) by A11,XREAL_1:7;
then ||.y-y1.|| + ||.y1-qy.|| < r by A21,XXREAL_0:2; then
||.y-qy.|| < r by A20,XXREAL_0:2; then
qy in Ball(y,r);
hence w in V by A1,A14,A19,ZFMISC_1:87;
end;
hence thesis by A9;
end;
hence V is open by NORMSP27;
end;
theorem LQ2:
for E,F be RealNormSpace,
Q be LinearOperator of E,F,
v be Point of E
st Q is one-to-one
holds Q.v = 0.F iff v = 0.E
proof
let E,F be RealNormSpace,
Q be LinearOperator of E,F,
v be Point of E;
assume
A1: Q is one-to-one;
hereby
assume
A2: Q.v = 0.F;
A3: dom Q = the carrier of E by FUNCT_2:def 1;
Q.(0.E) = 0.F by LOPBAN_7:3;
hence v = 0.E by A1,A2,A3,FUNCT_1:def 4;
end;
assume v = 0.E;
hence Q.v = 0.F by LOPBAN_7:3;
end;
theorem OP1:
for E be RealNormSpace,
X,Y be Subset of E,
v be Point of E
st X is open
& Y = {x+v where x is Point of E : x in X}
holds Y is open
proof
let E be RealNormSpace,
X,Y be Subset of E,
v be Point of E;
assume that
A1: X is open and
A2: Y = {x+v where x is Point of E : x in X};
deffunc FHP(Point of E) = 1 * $1 + (-v);
consider H being Function of E, E such that
A3: for p being Point of E holds H.p = FHP(p) from FUNCT_2:sch 4;
A4: dom H = the carrier of E by FUNCT_2:def 1;
for p be Point of E st p in the carrier of E
holds H/.p = 1*p +(-v) by A3; then
A5: H is_continuous_on the carrier of E by A4,NFCONT_1:52;
reconsider H1 = H as Function of TopSpaceNorm E,TopSpaceNorm E;
A6: H1 is continuous by A5,NORMSP_2:19;
reconsider X1 = X, Y1 = Y as Subset of TopSpaceNorm E;
A7: X1 is open by A1,NORMSP_2:16;
[#] TopSpaceNorm E <> {}; then
H1"X1 is open by A6,A7,TOPS_2:43; then
A9: H"X is open by NORMSP_2:16;
for s be object holds s in H"X iff s in Y
proof
let s be object;
hereby
assume
A10: s in H"X; then
A11: s in dom H & H.s in X by FUNCT_1:def 7;
reconsider s1=s as Point of E by A10;
A12: H.s = 1*s1 +(-v) by A3
.= s1 - v by RLVECT_1:def 8;
A13: H.s = H/.s by A11,PARTFUN1:def 6; then
H/.s + v = s1 - (v-v) by A12,RLVECT_1:29
.= s1-0.E by RLVECT_1:15
.= s1 by RLVECT_1:13;
hence s in Y by A2,A11,A13;
end;
assume s in Y; then
consider x be Point of E such that
A14: s = x+v & x in X by A2;
reconsider s1 = s as Point of E by A14;
H.s1 = 1*s1 +(-v) by A3
.= x+v -v by A14,RLVECT_1:def 8
.= x +(v-v) by RLVECT_1:28
.= x + 0.E by RLVECT_1:15
.= x by RLVECT_1:def 4;
hence s in H"X by A4,A14,FUNCT_1:def 7;
end;
hence thesis by A9,TARSKI:2;
end;
theorem OP2:
for E be RealNormSpace,
X,Y be Subset of E,
v be Point of E
st X is open & Y = {x-v where x is Point of E : x in X}
holds Y is open
proof
let E be RealNormSpace,
X,Y be Subset of E,
v be Point of E;
assume that
A1: X is open and
A2: Y = {x-v where x is Point of E : x in X};
set w = -v;
{x+w where x is Point of E : x in X} c= the carrier of E
proof
let s be object;
assume s in {x+w where x is Point of E : x in X}; then
ex x be Point of E st s=x+w & x in X;
hence s in the carrier of E;
end; then
reconsider Z = {x+w where x is Point of E : x in X} as Subset of E;
deffunc F(Point of E) = $1+w;
deffunc G(Point of E) = $1-v;
defpred P[Point of E] means $1 in X;
A3: for v being Element of the carrier of E holds F(v) = G(v);
{F(v1) where v1 is Element of the carrier of E : P[v1]}
= {G(v2) where v2 is Element of the carrier of E : P[v2]}
from FRAENKEL:sch 5 (A3);
hence thesis by A1,A2,OP1;
end;
begin :: 3. Existence and uniqueness of continuous implicit function
theorem FIXPOINT:
for X be RealBanachSpace,
S be non empty Subset of X,
f be PartFunc of X,X
st S is closed & dom f = S & rng f c= S
& ex k be Real
st 0 < k < 1
& for x,y be Point of X st x in S & y in S
holds ||. f/.x - f/.y .|| <= k * ||.x-y.||
holds
(ex x0 be Point of X st x0 in S & f.x0 = x0)
&(for x0,y0 be Point of X st x0 in S & y0 in S & f.x0 = x0 & f.y0 = y0
holds x0 = y0)
proof
let X be RealBanachSpace,
S be non empty Subset of X,
f be PartFunc of X,X;
assume that
A1: S is closed and
A2: dom f = S & rng f c= S and
A3: ex k be Real
st 0 < k < 1
& for x,y be Point of X st x in S & y in S
holds ||. f/.x - f/.y .|| <= k * ||.x-y.||;
consider x0 be object such that
A4: x0 in S by XBOOLE_0:def 1;
reconsider x0 as Element of X by A4;
consider K be Real such that
A5: 0 < K and
A6: K < 1 and
A7: for x,y be Point of X st x in S & y in S
holds ||.f/.x - f/.y.|| <= K * ||.x - y.|| by A3;
deffunc G(set,set)=f.$2;
consider g be Function such that
A8: dom g = NAT & g.0 = x0 & for n being Nat holds g.(n+1) = G(n,g.n)
from NAT_1:sch 11;
defpred P[Nat] means g.$1 in S & g.$1 is Element of X;
A9: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A10: P[k];
A11: g.(k+1)=f.(g.k) by A8;
f.(g.k) in rng f by A2,A10,FUNCT_1:3;
hence thesis by A2,A11;
end;
A12: P[0] by A4,A8;
A13: for n be Nat holds P[n] from NAT_1:sch 2(A12,A9);
for n be object st n in NAT holds g.n in the carrier of X
proof
let n be object such that
A14: n in NAT;
reconsider k = n as Nat by A14;
g.k is Element of X by A13;
hence thesis;
end; then
reconsider g as sequence of X by A8,FUNCT_2:3;
for x being Element of NAT holds g.x in S by A13; then
A15: rng g c= S by FUNCT_2:114;
A16: for n be Nat
holds ||.g.(n+1) - g.n .|| <= ||. g.1-g.0 .|| * (K to_power n)
proof
defpred P[Nat] means
||.g.($1+1) - g.($1) .|| <= ||. g.1-g.0 .|| * (K to_power $1);
A17: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
A18: g.(k+1) in S & g.k in S by A13;
A19: f/.(g.(k+1)) = f.(g.(k+1)) & f/. (g.k) = f. (g.k)
by A2,A13,PARTFUN1:def 6;
assume P[k]; then
A20: K * ||. g.(k+1) - g.k .||
<= K * (||. g.1-g.0 .|| * (K to_power k)) by A5,XREAL_1:64;
||.f/.(g.(k+1)) - f/.(g.k) .||
<= K * ||. g.(k+1) - g.k .|| by A7,A18; then
||.f/.(g.(k+1)) - f/.(g.k).||
<= ||. g.1-g.0 .|| * (K * (K to_power k)) by A20,XXREAL_0:2; then
A21: ||.f/.(g.(k+1)) - f/.(g.k) .||
<= ||. g.1-g.0 .|| * ((K to_power 1) * (K to_power k)) by POWER:25;
g.(k+1) =f.(g.k) by A8; then
||.g.((k+1)+1) - g.(k+1).||
= ||.f/.(g.(k+1)) - f/.(g.k) .|| by A8,A19;
hence thesis by A5,A21,POWER:27;
end;
||. g.(0+1) - g.(0) .|| = ||. g.1-g.0 .|| * 1
.= ||. g.1-g.0 .|| * (K to_power 0 ) by POWER:24; then
A22: P[0];
for n be Nat holds P[n] from NAT_1:sch 2(A22,A17);
hence thesis;
end;
A23: for k,n be Nat holds
||.g.(n+k) - g.n.|| <= ||. g.1-g.0 .||
* ((K to_power n - K to_power (n+k)) / (1-K))
proof
defpred P[Nat] means
for n be Nat holds ||. g.(n+$1) - g.n .|| <= ||. g.1-g.0 .||
* ((K to_power n-K to_power (n+$1)) /(1-K));
A24: now
let k be Nat such that
A25: P[k];
now
let n be Nat;
1-K <> 0 by A6; then
A26: ||. g.1-g.0 .|| * ((K to_power n - K to_power (n+k)) /(1-K))
+ ||. g.1-g.0 .|| * (K to_power (n+k))
= ||. g.1-g.0 .|| * ((K to_power n - K to_power (n+k))/(1-K))
+ ||. g.1-g.0 .|| * (K to_power (n+k)) * (1-K)/(1-K)
by XCMPLX_1:89
.= ||. g.1-g.0 .|| * ((K to_power n - K to_power (n+k))/(1-K))
+ ||. g.1-g.0 .|| * ((K to_power (n+k))*(1-K))/(1-K)
.= ||. g.1-g.0 .|| * ((K to_power n - K to_power (n+k))/(1-K))
+ ||. g.1-g.0 .|| * ((K to_power (n+k)*(1-K))/(1-K))
by XCMPLX_1:74
.= ||. g.1-g.0 .|| * (((K to_power n - K to_power (n+k))/(1-K))
+ ((K to_power (n+k)*(1-K))/(1-K)))
.= ||. g.1-g.0 .|| * (((K to_power n - K to_power (n+k))
+ (K to_power (n+k)*(1-K)))/(1-K)) by XCMPLX_1:62
.= ||. g.1-g.0 .|| * ((K to_power n - K*K to_power (n+k))/(1-K))
.= ||. g.1-g.0 .|| * ((K to_power n - (K to_power 1) *
K to_power (n+k)) /(1-K)) by POWER:25
.= ||. g.1-g.0 .|| * ((K to_power n - K to_power (n+k+1))/(1-K))
by A5,POWER:27;
||.g.(n+k) - g.n .||
<= ||. g.1-g.0 .|| * ((K to_power n - K to_power (n+k)) / (1-K))
& ||.g.((n+k)+1) - g.(n+k) .||
<= ||. g.1-g.0 .||* (K to_power (n+k)) by A16,A25; then
||.g.(n+(k+1)) - g.n .||
<= ||.g.(n+(k+1)) - g.(n+k) .|| + ||.g.(n+k) - g.n .||
& ||.g.(n+(k+1)) - g.(n+k) .|| + ||.g.(n+k) - g.n .||
<= ||. g.1-g.0 .|| * (K to_power (n+k))
+ ||. g.1-g.0 .|| * ((K to_power n - K to_power (n+k)) /(1-K))
by NORMSP_1:10,XREAL_1:7;
hence ||.g.(n+(k+1)) - g.n .||
<= ||. g.1-g.0 .||*((K to_power n - K to_power (n+(k+1)))/(1-K))
by A26,XXREAL_0:2;
end;
hence P[k+1];
end;
now
let n be Nat;
||.g.(n+0) - g.n .|| = ||.0.X.|| by RLVECT_1:15
.= 0;
hence ||.g.(n+0) - g.n .||
<= ||. g.1-g.0 .||* ((K to_power n - K to_power (n+0))/(1-K));
end; then
A27: P[0];
for k be Nat holds P[k] from NAT_1:sch 2(A27,A24);
hence thesis;
end;
A28: for k,n be Nat holds
||.g.(n+k) - g.n .|| <= ||. g.1-g.0 .|| * (K to_power n /(1-K))
proof
let k be Nat;
now
let n be Nat;
K to_power (n+k) > 0 by A5,POWER:34; then
A29: K to_power n - K to_power (n+k) <= K to_power n - 0 by XREAL_1:13;
1-K > 1-1 by A6,XREAL_1:15; then
(K to_power n - K to_power (n+k)) / (1-K)
<= (( K to_power n ) /(1-K)) by A29,XREAL_1:72; then
A30: ||. g.1-g.0 .|| * ((K to_power n - K to_power (n+k))/(1-K))
<= ||. g.1-g.0 .|| * (( K to_power n ) /(1-K)) by XREAL_1:64;
||. g.(n+k) - g.n .||
<= ||. g.1-g.0 .|| * ((K to_power n - K to_power (n+k))/(1-K)) by A23;
hence ||.g.(n+k) - g.n .||
<= ||. g.1-g.0 .|| * ((K to_power n)/(1-K)) by A30,XXREAL_0:2;
end;
hence thesis;
end;
now
let e be Real such that
A31: e > 0;
e/2 > 0 by A31,XREAL_1:215; then
consider n be Nat such that
A32: |. ||. g.1-g.0 .|| / (1-K) * (K to_power n) .| < e/2
by A5,A6,NFCONT_2:16;
reconsider nn=n+1 as Nat;
take nn;
||. g.1-g.0 .|| / (1-K)* (K to_power n)
<= |. ||. g.1-g.0 .|| / (1-K)* (K to_power n) .| by ABSVALUE:4; then
||. g.1-g.0 .|| / (1-K)* (K to_power n) < e/2 by A32,XXREAL_0:2; then
A33: ||. g.1-g.0 .|| *( (K to_power n)/(1-K)) < e/2 by XCMPLX_1:75;
now
let m,l be Nat such that
A34: nn <= m and
A35: nn <= l;
n < m by A34,NAT_1:13; then
consider k1 being Nat such that
A36: n+k1 = m by NAT_1:10;
n < l by A35,NAT_1:13; then
consider k2 being Nat such that
A37: n+k2 =l by NAT_1:10;
reconsider k2 as Nat;
||. g.(n+k2) - g.n .||
<= ||. g.1-g.0 .|| * ((K to_power n) /(1-K)) by A28; then
A38: ||.g.l - g.n .|| < e/2 by A33,A37,XXREAL_0:2;
reconsider k1 as Nat;
||.g.(n+k1) - g.n .|| <= ||. g.1-g.0 .|| * ((K to_power n)/(1-K))
by A28; then
||.g.m - g.n.|| < e/2 by A33,A36,XXREAL_0:2;
hence ||.g.l - g.m.|| < e by A31,A38,NDIFF_2:4;
end;
hence for n, m be Nat st n >= nn & m >= nn holds ||.g.n - g.m.|| < e;
end; then
A39: g is convergent by LOPBAN_1:def 15,RSSPACE3:8; then
A40: K(#)||. g - lim g .|| is convergent by NORMSP_1:24,SEQ_2:7;
A41: lim g in S by A1,A15,A39,NFCONT_1:def 3;
A42: now
let n be Nat;
A43: g.n in S by A13;
A44: f/.(g.n) = f.(g.n) & f/.(lim g) = f.(lim g)
by A1,A2,A13,A15,A39,NFCONT_1:def 3,PARTFUN1:def 6;
||. (g^\1).n - f/. (lim g) .||
= ||. g.(n+1) - f/. (lim g) .|| by NAT_1:def 3
.= ||. f/.(g.n)- f/. (lim g) .|| by A8,A44;
hence ||. (g^\1).n - f/.(lim g) .||
<= K * ||. g.n - lim g .|| by A7,A41,A43;
end;
A45: lim (K(#)(||.g - lim g.||))
= K * lim ||.(g - lim g).|| by A39,NORMSP_1:24,SEQ_2:8
.= K*0 by A39,NORMSP_1:24
.= 0;
A46: for e be Real st e >0
ex n be Nat st for m be Nat
st n<=m holds ||. (g^\1).m - f/.(lim g) .|| < e
proof
let e be Real;
assume e > 0; then
consider n be Nat such that
A47: for m be Nat st n <= m
holds |. (K(#)||. g - lim g .||).m - 0 .| < e
by A40,A45,SEQ_2:def 7;
take n;
now
let m be Nat;
assume n <= m; then
|. (K(#)||. g - lim g .||).m-0 .| < e by A47; then
|. K*||. g - lim g .||.m.| < e by SEQ_1:9; then
|. K*||. (g - lim g).m .||.| < e by NORMSP_0:def 4; then
A48: |. K*||. g.m - lim g .||.| < e by NORMSP_1:def 4;
K * ||. g.m - lim g .|| <= |. K*||. g.m - lim g .||.| by ABSVALUE:4;
then
A49: K*||. g.m - lim g .|| < e by A48,XXREAL_0:2;
||. (g^\1).m - f/.(lim g) .|| <= K* ||. g.m - lim g .|| by A42;
hence ||. (g^\1).m - f/. (lim g) .|| < e by A49,XXREAL_0:2;
end;
hence thesis;
end;
set xp = lim g;
A50: g^\1 is convergent & lim (g^\1) = lim g by A39,LOPBAN_3:9; then
A51: lim g = f/.(lim g) by A46,NORMSP_1:def 7;
A52:
now
let x be Point of X such that
A53: x in S & f.x = x;
A54: f/.x = x by A2,A53,PARTFUN1:def 6;
A55: for k be Nat holds ||.x-xp.|| <= ||.x-xp.|| * (K to_power k)
proof
defpred P[Nat] means
||.x-xp .|| <= ||.x-xp.||*(K to_power $1);
A56: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k]; then
A57: K * ||. x-xp .|| <= K * (||.x-xp.||*(K to_power k))
by A5,XREAL_1:64;
||. f/.x - f/.xp .|| <= K * ||. x-xp .|| by A7,A41,A53; then
||. f/.x - f/.xp .|| <= ||. x-xp .|| * (K * (K to_power k))
by A57,XXREAL_0:2; then
||. f/.x - f/.xp .||
<= ||. x-xp .|| * ((K to_power 1) * (K to_power k)) by POWER:25;
hence thesis by A5,A51,A54,POWER:27;
end;
||.x-xp .|| = ||. x-xp .|| * 1
.= ||. x-xp .|| * (K to_power 0) by POWER:24; then
A58: P[0];
for n be Nat holds P[n] from NAT_1:sch 2(A58,A56);
hence thesis;
end;
for e be Real st 0 < e holds ||.x-xp.|| < e
proof
let e be Real;
assume 0 < e; then
consider n be Nat such that
A59: |.||.x-xp.|| * (K to_power n) .| < e by A5,A6,NFCONT_2:16;
||.x-xp.|| * (K to_power n) <= |.||.x-xp.||*(K to_power n).|
by ABSVALUE:4; then
A60: ||.x-xp.|| * (K to_power n) < e by A59,XXREAL_0:2;
||.x-xp.|| <= ||.x-xp.||*(K to_power n) by A55;
hence thesis by A60,XXREAL_0:2;
end;
hence x=xp by NDIFF_2:4;
end;
xp = f/.xp by A46,A50,NORMSP_1:def 7; then
xp = f.xp by A1,A2,A15,A39,NFCONT_1:def 3,PARTFUN1:def 6;
hence ex x0 be Point of X st x0 in S & f.x0 = x0
by A1,A15,A39,NFCONT_1:def 3;
for x0,y0 be Point of X
st x0 in S & y0 in S & f.x0 = x0 & f.y0 = y0
holds x0=y0
proof
let x0,y0 be Point of X such that
A61: x0 in S and
A62: y0 in S and
A63: f.x0 = x0 and
A64: f.y0 = y0;
x0 = xp by A52,A61,A63;
hence thesis by A52,A62,A64;
end;
hence thesis;
end;
theorem FIXPOINT2:
for E be RealNormSpace,
F be RealBanachSpace,
E0 be non empty Subset of E,
F0 be non empty Subset of F,
Fai be PartFunc of [:E,F:],F
st F0 is closed
& [:E0,F0:] c= dom Fai
& (for x be Point of E, y be Point of F
st x in E0 & y in F0
holds Fai.(x,y) in F0)
& (for y be Point of F st y in F0 holds
for x0 be Point of E st x0 in E0
for e be Real st 0 < e
ex d be Real
st 0 < d
& for x1 be Point of E
st x1 in E0
& ||.x1-x0.|| < d
holds ||. Fai/.[x1,y] - Fai/.[x0,y] .|| < e )
& ex k be Real
st 0 < k & k < 1
& (for x be Point of E st x in E0 holds
for y1,y2 be Point of F st y1 in F0 & y2 in F0
holds ||. Fai/.[x,y1] - Fai/.[x,y2] .|| <= k * ||.y1-y2.||)
holds
(for x be Point of E st x in E0
holds
(ex y be Point of F st y in F0 & Fai.(x,y) = y)
& (for y1,y2 be Point of F
st y1 in F0 & y2 in F0 & Fai.(x,y1) = y1 & Fai.(x,y2) = y2
holds y1 = y2))
& (for x0 be Point of E, y0 be Point of F
st x0 in E0 & y0 in F0 & Fai.(x0,y0) = y0
holds
(for e be Real st 0 < e holds
ex d be Real
st 0 < d
& (for x1 be Point of E, y1 be Point of F
st x1 in E0 & y1 in F0 & Fai.(x1,y1) = y1
& ||.x1-x0.|| < d
holds ||.y1-y0.|| < e)))
proof
let E be RealNormSpace,
F be RealBanachSpace,
E0 be non empty Subset of E,
F0 be non empty Subset of F,
Fai be PartFunc of [:E,F:],F such that
A1: F0 is closed and
A2: [:E0,F0:] c= dom Fai and
A3: for x be Point of E, y be Point of F
st x in E0 & y in F0 holds Fai.(x,y) in F0 and
A4: for y be Point of F st y in F0 holds
for x0 be Point of E st x0 in E0
for e be Real st 0 < e
ex d be Real
st 0 < d
& for x1 be Point of E
st x1 in E0
& ||.x1-x0.|| < d
holds ||. Fai/.[x1,y] - Fai/.[x0,y] .|| < e and
A5: ex k be Real
st 0 < k & k < 1
& for x be Point of E st x in E0 holds
for y1,y2 be Point of F st y1 in F0 & y2 in F0
holds ||. Fai/.[x,y1] - Fai/.[x,y2] .|| <= k * ||.y1-y2.||;
consider k be Real such that
A6: 0 < k & k < 1 and
A7: for x be Point of E st x in E0 holds
for y1,y2 be Point of F st y1 in F0 & y2 in F0
holds ||. Fai/.[x,y1] - Fai/.[x,y2] .|| <= k * ||.y1-y2.|| by A5;
thus for x be Point of E st x in E0 holds
(ex y be Point of F st y in F0 & Fai.(x,y) = y)
& (for y1,y2 be Point of F
st y1 in F0 & y2 in F0 & Fai.(x,y1) = y1 & Fai.(x,y2) = y2
holds y1 = y2)
proof
let x be Point of E;
deffunc FX1(object) = Fai.(x,$1);
assume
A8: x in E0; then
A9: for y being object st y in F0 holds FX1(y) in F0 by A3;
consider Fai0 being Function of F0,F0 such that
A10: for y being object st y in F0 holds
Fai0 . y = FX1(y) from FUNCT_2:sch 2(A9);
A11: rng Fai0 c= F0;
A12: dom Fai0 = F0 by FUNCT_2:def 1;
rng Fai0 c= the carrier of F by XBOOLE_1:1; then
reconsider Fai0 as PartFunc of F,F by A12,RELSET_1:4;
A13: for z,y be Point of F st z in F0 & y in F0
holds ||.Fai0/.z - Fai0/.y .|| <= k * ||.z-y.||
proof
let z,y be Point of F;
assume
A14: z in F0 & y in F0; then
A15: [x,z] in [:E0,F0:] by A8,ZFMISC_1:87;
A16: [x,y] in [:E0,F0:] by A8,A14,ZFMISC_1:87;
A18: y in dom Fai0 by A14,FUNCT_2:def 1;
z in dom Fai0 by A14,FUNCT_2:def 1; then
A19: Fai0/.z = Fai0 . z by PARTFUN1:def 6
.= FX1(z) by A10,A14
.= Fai/.[x,z] by A2,A15,PARTFUN1:def 6;
Fai0/.y = Fai0 . y by A18,PARTFUN1:def 6
.= FX1(y) by A10,A14
.= Fai/.[x,y] by A2,A16,PARTFUN1:def 6;
hence thesis by A7,A8,A14,A19;
end;
thus ex y be Point of F st y in F0 & Fai.(x,y) = y
proof
consider y be Point of F such that
A20: y in F0 & Fai0.y = y by A1,A6,A11,A12,A13,FIXPOINT;
take y;
thus y in F0 by A20;
thus Fai.(x,y) = y by A10,A20;
end;
thus for y1,y2 be Point of F
st y1 in F0 & y2 in F0
& Fai.(x,y1) = y1 & Fai.(x,y2) = y2
holds y1 = y2
proof
let y1,y2 be Point of F such that
A21: y1 in F0
& y2 in F0
& Fai.(x,y1) = y1
& Fai.(x,y2) = y2;
A22: Fai0.y1 = y1 by A10,A21;
Fai0.y2 = y2 by A10,A21;
hence y1 = y2 by A1,A6,A11,A12,A13,A21,A22,FIXPOINT;
end;
end;
thus for x0 be Point of E, y0 be Point of F
st x0 in E0 & y0 in F0 & Fai.(x0,y0) = y0
holds
(for e be Real st 0 < e holds
ex d be Real
st 0 < d
& (for x1 be Point of E, y1 be Point of F
st x1 in E0 & y1 in F0 & Fai.(x1,y1) = y1
& ||.x1-x0.|| < d
holds ||.y1-y0.|| < e))
proof
let x0 be Point of E, y0 be Point of F;
assume
A24: x0 in E0 & y0 in F0 & Fai.(x0,y0) = y0;
let e be Real;
assume
A25: 0 < e;
reconsider e1 = e*(1-k) as Real;
A26: 0 < 1 - k by A6,XREAL_1:50; then
consider d be Real such that
A27: 0 < d
& for x1 be Point of E
st x1 in E0
& ||.x1-x0.|| < d
holds ||. Fai/.[x1,y0] - Fai/.[x0,y0] .|| < e1
by A4,A24,A25,XREAL_1:129;
take d;
thus 0 < d by A27;
let x1 be Point of E, y1 be Point of F;
assume
A28: x1 in E0 & y1 in F0 & Fai.(x1,y1) = y1 & ||.x1-x0.|| < d;
[x0,y0] in [:E0,F0:] by A24,ZFMISC_1:87; then
A29: y0 = Fai/. [x0,y0] by A2,A24,PARTFUN1:def 6;
[x1,y1] in [:E0,F0:] by A28,ZFMISC_1:87; then
A30: y1 = Fai/. [x1,y1] by A2,A28,PARTFUN1:def 6;
(Fai/. [x1,y1] -Fai/. [x1,y0]) + (Fai/. [x1,y0] -Fai/. [x0,y0])
= (Fai/. [x1,y1] -Fai/. [x1,y0] + Fai/. [x1,y0])
- Fai/. [x0,y0] by RLVECT_1:28
.= Fai/. [x1,y1] -Fai/. [x0,y0] by RLVECT_4:1; then
A31: ||.y1-y0.|| <= ||.Fai/. [x1,y1] - Fai/. [x1,y0] .||
+ ||.Fai/. [x1,y0] - Fai/. [x0,y0] .||
by A29,A30,NORMSP_1:def 1;
||.Fai/. [x1,y0] - Fai/. [x0,y0] .|| < e1 by A27,A28; then
||. Fai /. [x1,y1] - Fai/. [x1,y0] .||
+ ||. Fai /. [x1,y0] - Fai/. [x0,y0] .||
< e1 + k* ||. y1 - y0 .|| by A7,A24,A28,XREAL_1:8; then
||.y1-y0.|| < e1 + k * ||. y1-y0 .|| by A31,XXREAL_0:2; then
||.y1-y0.|| - k * ||. y1-y0 .||
< e1 + k * ||. y1-y0 .|| - k * ||. y1-y0 .|| by XREAL_1:14; then
(1-k)* ||.y1-y0.|| < e1; then
||.y1-y0.|| < e1/(1-k) by A26,XREAL_1:81;
hence ||.y1-y0.|| < e by A26,XCMPLX_1:89;
end;
end;
theorem FIXPOINT3:
for E be RealNormSpace,
F be RealBanachSpace,
A be non empty Subset of E,
B be non empty Subset of F,
Fai be PartFunc of [:E,F:],F
st B is closed
& [:A,B:] c= dom Fai
& (for x be Point of E, y be Point of F
st x in A & y in B holds Fai.(x,y) in B )
& (for y be Point of F st y in B holds
for x0 be Point of E st x0 in A
for e be Real st 0 < e
ex d be Real
st 0 < d
& for x1 be Point of E
st x1 in A & ||.x1-x0.|| < d
holds ||. Fai/.[x1,y] - Fai/.[x0,y] .|| < e)
& ex k be Real
st 0 < k & k < 1
& (for x be Point of E st x in A holds
for y1,y2 be Point of F st y1 in B & y2 in B
holds ||. Fai/.[x,y1] - Fai/.[x,y2] .|| <= k * ||.y1-y2.||)
holds
(ex g be PartFunc of E,F
st g is_continuous_on A
& dom g = A & rng g c= B
& for x be Point of E st x in A
holds Fai.(x,g.x) = g.x)
&(for g1,g2 be PartFunc of E,F
st dom g1 = A & rng g1 c= B
& dom g2 = A & rng g2 c= B
&(for x be Point of E st x in A holds Fai.(x,g1.x) = g1.x)
&(for x be Point of E st x in A holds Fai.(x,g2.x) = g2.x)
holds g1=g2)
proof
let E be RealNormSpace,
F be RealBanachSpace,
A be non empty Subset of E,
B be non empty Subset of F,
Fai be PartFunc of [:E,F:],F such that
A1: B is closed and
A2: [:A,B:] c= dom Fai and
A3: for x be Point of E, y be Point of F
st x in A & y in B holds Fai.(x,y) in B and
A4: for y be Point of F st y in B holds
for x0 be Point of E st x0 in A
for e be Real st 0 < e
ex d be Real
st 0 < d
& for x1 be Point of E
st x1 in A
& ||.x1-x0.|| < d
holds ||. Fai/.[x1,y] - Fai/.[x0,y] .|| < e and
A5: ex k be Real
st 0 < k & k < 1
& for x be Point of E st x in A holds
for y1,y2 be Point of F st y1 in B & y2 in B
holds ||. Fai/.[x,y1] - Fai/.[x,y2] .|| <= k * ||.y1-y2.||;
thus ex g be PartFunc of E,F
st g is_continuous_on A
& dom g = A & rng g c= B
& for x be Point of E st x in A
holds Fai.(x,g.x) = g.x
proof
defpred FP[object,object] means
$2 in B & Fai.($1,$2) = $2;
A6: for x,y1,y2 be object
st x in A & FP[x,y1] & FP[x,y2]
holds y1 = y2 by A1,A2,A3,A4,A5,FIXPOINT2;
A7: for x be object st x in A ex y be object st FP[x,y]
proof
let x be object;
assume
A8: x in A; then
reconsider x0 = x as Point of E;
consider y be Point of F such that
A9: y in B & Fai.(x0,y) = y by A1,A2,A3,A4,A5,A8,FIXPOINT2;
take y;
thus thesis by A9;
end;
consider g be Function such that
A10: dom g = A & for x be object st x in A holds FP[x,g.x]
from FUNCT_1:sch 2(A6,A7);
A11: rng g c= B
proof
let y be object;
assume y in rng g; then
consider x being object such that
A12: x in dom g & y = g.x by FUNCT_1:def 3;
thus y in B by A10,A12;
end; then
rng g c= the carrier of F by XBOOLE_1:1; then
g in PFuncs(the carrier of E,the carrier of F)
by A10,PARTFUN1:def 3; then
reconsider g as PartFunc of E,F by PARTFUN1:46;
take g;
for z0 being Point of E
for r being Real st z0 in A & 0 < r holds
ex s being Real
st 0 < s
& for z1 being Point of E
st z1 in A & ||.z1 - z0.|| < s
holds ||. g /. z1 - g /. z0.|| < r
proof
let z0 be Point of E;
let r be Real;
assume
A15: z0 in A & 0 < r; then
A16: Fai.(z0,g.z0) = g.z0 by A10;
A17: g.z0 in rng g by A10,A15,FUNCT_1:3;
g.z0 = g/.z0 by A10,A15,PARTFUN1:def 6; then
consider s be Real such that
A18: 0 < s
& for x1 be Point of E, y1 be Point of F
st x1 in A & y1 in B & Fai.(x1,y1) = y1
& ||.x1-z0.|| < s
holds ||.y1-g/.z0.|| < r
by A1,A2,A3,A4,A5,A11,A15,A16,A17,FIXPOINT2;
take s;
thus 0 < s by A18;
let z1 be Point of E;
assume
A19: z1 in A & ||.z1 - z0.|| < s; then
A20: Fai.(z1,g.z1) = g.z1 by A10;
A21: g.z1 in B by A10,A19;
g.z1 = g/.z1 by A10,A19,PARTFUN1:def 6;
hence ||. g /. z1 - g /. z0.|| < r by A18,A19,A20,A21;
end;
hence g is_continuous_on A by A10,NFCONT_1:19;
thus dom g = A & rng g c= B by A10,A11;
thus for x be Point of E st x in A
holds Fai.(x,g.x) = g.x by A10;
end;
let g1,g2 be PartFunc of E,F such that
A22: dom g1 = A & rng g1 c= B
& dom g2 = A & rng g2 c= B
& (for x be Point of E st x in A holds Fai.(x,g1.x) = g1.x)
& (for x be Point of E st x in A holds Fai.(x,g2.x) = g2.x);
for x being object st x in dom g1 holds g1.x = g2.x
proof
let x be object;
assume
A23:x in dom g1; then
reconsider y = x as Point of E;
A24: g1.y in rng g1 by A23,FUNCT_1:3; then
reconsider z1 = g1.y as Point of F;
A25: g2.y in rng g2 by A22,A23,FUNCT_1:3; then
reconsider z2 = g2.y as Point of F;
Fai.(y,z1) = z1 & Fai.(y,z2) = z2
& z1 in B & z2 in B & y in A by A22,A23,A24,A25;
hence g1.x = g2.x by A1,A2,A3,A4,A5,FIXPOINT2;
end;
hence g1 = g2 by A22,FUNCT_1:2;
end;
theorem
for E,F be RealNormSpace,
s1,s2 be Point of [:E,F:]
st s1`2 = s2`2
holds reproj1 s1 = reproj1 s2
proof
let E,F be RealNormSpace,
s1,s2 be Point of [:E,F:];
assume
A1: s1`2 = s2`2;
now
let r be Element of E;
thus (reproj1 s1) . r = [r,(s2 `2) ] by A1,NDIFF_7:def 1
.= (reproj1 s2) . r by NDIFF_7:def 1;
end;
hence thesis by FUNCT_2:63;
end;
theorem REP2:
for E,F be RealNormSpace,
s1,s2 be Point of [:E,F:]
st s1`1 = s2`1
holds reproj2 s1 = reproj2 s2
proof
let E,F be RealNormSpace,
s1,s2 be Point of [:E,F:];
assume
A1: s1`1 = s2`1;
now
let r be Element of F;
thus (reproj2 s1) . r = [(s2 `1),r ] by A1,NDIFF_7:def 2
.=(reproj2 s2) . r by NDIFF_7:def 2;
end;
hence thesis by FUNCT_2:63;
end;
theorem LMCLOSE2:
for E be RealNormSpace,
r be Real,
z,y1,y2 be Point of E
st y1 in cl_Ball(z,r) & y2 in cl_Ball(z,r)
holds [.y1,y2.] c= cl_Ball(z,r)
proof
let E be RealNormSpace,
r be Real,
z,y1,y2 be Point of E;
assume
A1: y1 in cl_Ball(z,r) & y2 in cl_Ball(z,r); then
A2: ex y1q be Element of E
st y1 = y1q & ||.z - y1q .|| <= r;
A3: ex y2q be Element of E
st y2 = y2q & ||.z - y2q.|| <= r by A1;
A4: [.y1,y2.]
= { (((1 - r) * y1) + (r * y2)) where r is Real : 0 <= r <= 1 }
by RLTOPSP1:def 2;
let s be object;
assume s in [.y1,y2.]; then
consider p be Real such that
A5: s = (1 - p) * y1 + (p * y2) & 0 <= p & p <= 1 by A4;
reconsider w = s as Point of E by A5;
(1 - p) * z + p * z = ((1-p)+p) * z by RLVECT_1:def 6
.= z by RLVECT_1:def 8; then
z - w
= (1 - p) * z + p * z - (1 - p) * y1 - (p * y2) by A5,RLVECT_1:27
.= (1 - p) * z + - (1 - p) * y1 + p * z - (p * y2) by RLVECT_1:def 3
.= ((1 - p) * z - (1 - p) * y1) +(p * z + - (p * y2)) by RLVECT_1:def 3
.= (1 - p) * (z - y1) + (p * z - p * y2) by RLVECT_1:34
.= (1 - p) * (z - y1) + p * (z -y2) by RLVECT_1:34; then
||.z - w.|| <= ||. (1 - p) * (z - y1) .|| + ||. p*(z -y2) .||
by NORMSP_1:def 1; then
||.z - w.|| <= |. 1-p .| * ||. z - y1 .|| + ||. p*(z -y2) .||
by NORMSP_1:def 1; then
A7: ||.z - w.|| <= |. 1-p .| * ||. z - y1 .|| + |.p.| *||. z -y2 .||
by NORMSP_1:def 1;
A8: |. 1 - p .| = 1 - p & |.p.| = p by A5,COMPLEX1:43,XREAL_1:48;
0 <= 1 - p by A5,XREAL_1:48; then
A9: (1 - p) * ||. z - y1 .|| <= (1 - p) * r by A2,XREAL_1:64;
p * ||. z -y2 .|| <= p * r by A3,A5,XREAL_1:64; then
(1 - p) * ||. z - y1 .|| + p * ||. z -y2 .|| <= (1 - p) * r + p * r
by A9,XREAL_1:7; then
||.z - w.|| <= (1 - p) * r + p * r by A7,A8,XXREAL_0:2;
hence thesis;
end;
theorem NEIB1:
for E be RealNormSpace,
x,b be Point of E,
N be Neighbourhood of x holds
{z-b where z is Point of E: z in N} is Neighbourhood of x-b &
{z+b where z is Point of E: z in N} is Neighbourhood of x+b
proof
let E be RealNormSpace,
x,b be Point of E,
N be Neighbourhood of x;
consider g being Real such that
A1: 0 < g
& { y where y is Point of E : ||.(y - x).|| < g } c= N by NFCONT_1:def 1;
set V = { y where y is Point of E : ||.(y - x).|| < g };
B2: {z-b where z is Point of E: z in N} c= the carrier of E
proof
let s be object;
assume s in {z-b where z is Point of E: z in N}; then
ex z be Point of E st s=z-b & z in N;
hence s in the carrier of E;
end;
B3: {z+b where z is Point of E: z in N} c= the carrier of E
proof
let s be object;
assume s in {z+b where z is Point of E: z in N}; then
ex z be Point of E st s=z+b & z in N;
hence s in the carrier of E;
end;
{y where y is Point of E : ||.(y - (x-b) ).|| < g} c=
{z-b where z is Point of E: z in N}
proof
let t be object;
assume t in {y where y is Point of E : ||.(y - (x-b) ).|| < g}; then
consider y be Point of E such that
A4: t=y & ||.(y - (x-b) ).|| < g;
(y - (x - b)) = (y - x) + b by RLVECT_1:29
.= y + b - x by RLVECT_1:def 3; then
A5: y + b in V by A4;
y = (y + b) - b by RLVECT_4:1;
hence t in {z-b where z is Point of E: z in N} by A1,A4,A5;
end;
hence {z-b where z is Point of E: z in N} is Neighbourhood of x-b
by A1,B2,NFCONT_1:def 1;
{y where y is Point of E : ||.(y - (x+b) ).|| < g} c=
{z+b where z is Point of E: z in N}
proof
let t be object;
assume t in {y where y is Point of E : ||.(y - (x+b) ).|| < g}; then
consider y be Point of E such that
A6: t = y & ||.(y - (x + b) ).|| < g;
||. (y - b) - x .|| < g by A6,RLVECT_1:27; then
A7: y - b in V;
y = (y - b) + b by RLVECT_4:1;
hence t in {z + b where z is Point of E: z in N} by A1,A6,A7;
end;
hence {z + b where z is Point of E: z in N} is Neighbourhood of x + b
by A1,B3,NFCONT_1:def 1;
end;
theorem Th1:
for E,G be RealNormSpace,
F be RealBanachSpace,
Z be Subset of [:E,F:],
f be PartFunc of [:E,F:], G,
a be Point of E,
b be Point of F,
c be Point of G,
z be Point of [:E,F:]
st Z is open & dom f = Z
& f is_continuous_on Z
& f is_partial_differentiable_on`2 Z
& f `partial`2|Z is_continuous_on Z
& z = [a,b] & z in Z
& f.(a,b) = c
& partdiff`2(f,z) is one-to-one
& partdiff`2(f,z)" is Lipschitzian LinearOperator of G,F
holds
ex r1,r2 be Real
st 0 < r1 & 0 < r2
& [:Ball(a,r1),cl_Ball(b,r2):] c= Z
& (for x be Point of E st x in Ball(a,r1) holds
ex y be Point of F st y in cl_Ball(b,r2) & f.(x,y) = c)
& (for x be Point of E st x in Ball(a,r1) holds
(for y1,y2 be Point of F
st y1 in cl_Ball(b,r2) & y2 in cl_Ball(b,r2)
& f.(x,y1) = c & f.(x,y2) = c
holds y1 = y2))
& (ex g be PartFunc of E,F
st g is_continuous_on Ball(a,r1)
& dom g = Ball(a,r1)
& rng g c= cl_Ball(b,r2)
& g.a = b
& for x be Point of E st x in Ball(a,r1)
holds f.(x,g.x) = c )
& (for g1,g2 be PartFunc of E,F
st dom g1 = Ball(a,r1)
& rng g1 c= cl_Ball(b,r2)
& (for x be Point of E st x in Ball(a,r1)
holds f.(x,g1.x) = c)
& dom g2 = Ball(a,r1)
& rng g2 c= cl_Ball(b,r2)
& (for x be Point of E st x in Ball(a,r1)
holds f.(x,g2.x) = c)
holds g1=g2)
proof
let E,G be RealNormSpace,
F be RealBanachSpace,
Z be Subset of [:E,F:],
f be PartFunc of [:E,F:], G,
a be Point of E,
b be Point of F,
c be Point of G,
z be Point of [:E,F:] such that
A1: Z is open and
A2: dom f = Z and
A3: f is_continuous_on Z and
A4: f is_partial_differentiable_on`2 Z and
A5: f `partial`2|Z is_continuous_on Z and
A6: z = [a,b] & z in Z and
A7: f.(a,b) = c and
A8: partdiff`2(f,z) is one-to-one and
A9: partdiff`2(f,z)" is Lipschitzian LinearOperator of G,F;
consider QQ be Lipschitzian LinearOperator of G,F such that
A10: QQ = (partdiff`2(f,z))" by A9;
reconsider Q = QQ as Point of R_NormSpace_of_BoundedLinearOperators(G,F)
by LOPBAN_1:def 9;
set BLQ = ||.Q.||;
reconsider z1 = [a,0.F] as Point of [:E,F:];
reconsider e0b = [0.E,b] as Point of [:E,F:];
A11: -e0b = [-0.E,-b] by PRVECT_3:18
.= [0.E,-b] by RLVECT_1:12;
deffunc FHP(Point of [:E,F:]) = 1 * $1 + (-e0b);
consider H being Function of the carrier of [:E,F:],the carrier of [:E,F:]
such that
A12: for p being Point of [:E,F:] holds H.p = FHP(p)
from FUNCT_2:sch 4;
A13: for x be Point of E,y be Point of F holds H.(x,y) = [x,y-b]
proof
let x be Point of E,y be Point of F;
reconsider p = [x,y] as Point of [:E,F:];
A14: 1*p = [1*x,1*y] by PRVECT_3:18
.= [x,1*y] by RLVECT_1:def 8
.= [x,y] by RLVECT_1:def 8;
thus H. (x,y) = 1 * p + (-e0b) by A12
.= [x+0.E,y+-b] by A11,A14,PRVECT_3:18
.= [x,y-b ] by RLVECT_1:def 4;
end;
A15: dom H = the carrier of [:E,F:] by FUNCT_2:def 1;
deffunc FKP(Point of [:E,F:]) = 1 * $1 + e0b;
consider K being Function of the carrier of [:E,F:],the carrier of [:E,F:]
such that
A16: for p being Point of [:E,F:] holds K.p = FKP(p)
from FUNCT_2:sch 4;
A17: dom K = the carrier of [:E,F:] by FUNCT_2:def 1;
for p be Point of [:E,F:] holds (K*H).p = p
proof
let p be Point of [:E,F:];
H.p = 1 * p + (-e0b) by A12
.= p -e0b by RLVECT_1:def 8; then
K.(H.p) = 1*(p -e0b) + e0b by A16
.= p -e0b + e0b by RLVECT_1:def 8
.= p -(e0b-e0b) by RLVECT_1:29
.= p - 0.[:E,F:] by RLVECT_1:15
.= p by RLVECT_1:13;
hence (K*H).p = p by A15,FUNCT_1:13;
end; then
A18: K*H = id(the carrier of [:E,F:]) by FUNCT_2:124; then
A19: H is one-to-one & K is onto by FUNCT_2:23;
for p be Point of [:E,F:] holds (H*K).p = p
proof
let p be Point of [:E,F:];
K.p = 1 * p + e0b by A16
.= p +e0b by RLVECT_1:def 8; then
H.(K.p) = 1*(p +e0b) - e0b by A12
.= p +e0b - e0b by RLVECT_1:def 8
.= p +(e0b-e0b) by RLVECT_1:28
.= p + 0.[:E,F:] by RLVECT_1:15
.= p by RLVECT_1:def 4;
hence (H*K).p = p by A17,FUNCT_1:13;
end; then
H*K = id(the carrier of [:E,F:]) by FUNCT_2:124; then
K is one-to-one & H is onto by FUNCT_2:23; then
rng H = the carrier of [:E,F:] by FUNCT_2:def 3; then
A20: K = H" by A18,FUNCT_2:23,FUNCT_2:30;
reconsider Z1 = H.: Z as Subset of [:E,F:];
A21: for x be Point of E,y be Point of F
holds [x,y+b] in Z iff [x,y] in Z1
proof
let x be Point of E,y be Point of F;
hereby
assume
A22: [x,y+b] in Z;
reconsider q = [x,y+b] as Point of [:E,F:];
q in the carrier of [:E,F:]; then
A23: [x,y+b] in dom H by FUNCT_2:def 1;
H. [x,y+b] = H.(x,y+b)
.= [x,y+b-b] by A13
.= [x,y+(b-b) ] by RLVECT_1:28
.= [x,y+0.F ] by RLVECT_1:15
.= [x,y] by RLVECT_1:def 4;
hence [x,y] in Z1 by A22,A23,FUNCT_1:def 6;
end;
assume [x,y] in Z1; then
consider s being object such that
A24: s in dom H & s in Z & [x,y] = H.s by FUNCT_1:def 6;
consider x1 be Point of E,y1 be Point of F such that
A25: s = [x1,y1] by A24,PRVECT_3:18;
A26: H. [x1,y1] = H.(x1,y1)
.= [x1,y1-b] by A13; then
x = x1 & y = y1-b by A24,A25,XTUPLE_0:1; then
y + b = y1 - (b - b) by RLVECT_1:29
.= y1 - 0.F by RLVECT_1:5
.= y1 by RLVECT_1:13;
hence [x,y+b] in Z by A24,A25,A26,XTUPLE_0:1;
end;
reconsider e0b = [0.E,b] as Point of [:E,F:];
A27: for p be object holds
p in Z1 iff p in { y-e0b where y is Point of [:E,F:] : y in Z}
proof
let p be object;
A28: -e0b = [-0.E,-b] by PRVECT_3:18
.= [0.E,-b] by RLVECT_1:12;
hereby
assume
A29: p in Z1; then
consider s be Point of E,t be Point of F such that
A30: p = [s,t] by PRVECT_3:18;
A31: [s,t+b] in Z by A21,A29,A30;
reconsider y = [s,t+b] as Point of [:E,F:];
y - e0b = [s+0.E,t+b + -b] by A28,PRVECT_3:18
.= [s,t+b -b] by RLVECT_1:def 4
.= [s,t+(b-b) ] by RLVECT_1:28
.= [s,t+0.F ] by RLVECT_1:15
.= p by A30,RLVECT_1:def 4;
hence p in { y-e0b where y is Point of [:E,F:] : y in Z} by A31;
end;
assume p in {y-e0b where y is Point of [:E,F:] : y in Z}; then
consider y be Point of [:E,F:] such that
A32: p = y-e0b & y in Z;
consider s be Point of E,t be Point of F such that
A33: y = [s,t] by PRVECT_3:18;
A34: p = [s+0.E,t + -b] by A28,A32,A33,PRVECT_3:18
.= [s,t-b] by RLVECT_1:def 4;
t-b + b = t -(b-b ) by RLVECT_1:29
.= t -0.F by RLVECT_1:15
.= t by RLVECT_1:13;
hence p in Z1 by A21,A32,A33,A34;
end; then
A35: Z1 = {y-e0b where y is Point of [:E,F:] : y in Z} by TARSKI:2;
A36: Z1 is open by A1,A27,OP2,TARSKI:2;
defpred FP1[object,object] means
ex x be Point of E, y be Point of F
st $1 = [x,y] & $2 = f/.[x,y+b] - c;
A37:for p be object st p in Z1
ex w be object st w in the carrier of G & FP1[p,w]
proof
let p be object;
assume p in Z1; then
consider x be Point of E,y be Point of F such that
A38: p = [x,y] by PRVECT_3:18;
f/.[x,y+b] - c is Point of G;
hence thesis by A38;
end;
consider f1 being Function of Z1,G such that
A39: for p being object st p in Z1 holds FP1[p,f1.p]
from FUNCT_2:sch 1(A37);
A40: rng f1 c= the carrier of G;
A41: dom f1 = Z1 by FUNCT_2:def 1; then
f1 in PFuncs(the carrier of [:E,F:],the carrier of G)
by A40,PARTFUN1:def 3; then
reconsider f1 as PartFunc of [:E,F:], G by PARTFUN1:46;
A42: for x be Point of E, y be Point of F st [x,y] in Z1
holds f1.(x,y) = f/.[x,y+b] - c
proof
let x be Point of E,
y be Point of F;
assume [x,y] in Z1; then
consider x0 be Point of E,y0 be Point of F such that
A43: [x,y] = [x0,y0]
& f1.([x,y]) = f/.[x0,y0+b] - c by A39;
x = x0 & y = y0 by A43,XTUPLE_0:1;
hence thesis by A43;
end;
defpred FP2[object,object] means
ex x be Point of E, y be Point of F
st $1 = [x,y] & $2=Q.(f1.(x,y));
A44: for p be object st p in Z1
ex w be object st w in the carrier of F & FP2[p,w]
proof
let p be object;
assume
A45: p in Z1; then
consider x be Point of E,y be Point of F such that
A46: p = [x,y] by PRVECT_3:18;
A47: Q.(f1/.[x,y]) is Point of F;
[x,y] in dom f1 by A45,A46,FUNCT_2:def 1; then
f1/.[x,y] = f1.(x,y) by PARTFUN1:def 6;
hence thesis by A46,A47;
end;
consider f2 being Function of Z1,F such that
A48: for p being object st p in Z1 holds FP2[p,f2.p]
from FUNCT_2:sch 1(A44);
A49: rng f2 c= the carrier of F;
A50: dom f2 = Z1 by FUNCT_2:def 1; then
f2 in PFuncs(the carrier of [:E,F:],the carrier of F)
by A49,PARTFUN1:def 3; then
reconsider f2 as PartFunc of [:E,F:], F by PARTFUN1:46;
A51: for x be Point of E, y be Point of F st [x,y] in Z1
holds f2.(x,y) = Q.(f1.(x,y))
proof
let x be Point of E,
y be Point of F;
assume [x,y] in Z1; then
consider x0 be Point of E,y0 be Point of F such that
A52: [x,y] = [x0,y0]
& f2.([x,y]) = Q.(f1.(x0,y0)) by A48;
thus thesis by A52;
end;
defpred FP3[object,object] means
ex x be Point of E, y be Point of F
st $1 = [x,y] & $2 = y-f2/.[x,y];
A53: for p be object st p in Z1
ex w be object st w in the carrier of F & FP3[p,w]
proof
let p be object;
assume p in Z1; then
consider x be Point of E,y be Point of F such that
A54: p = [x,y] by PRVECT_3:18;
y - f2/.[x,y] is Point of F;
hence thesis by A54;
end;
consider Fai being Function of Z1,F such that
A55: for p being object st p in Z1 holds FP3[p,Fai.p]
from FUNCT_2:sch 1(A53);
A56: rng Fai c= the carrier of F;
A57: dom Fai = Z1 by FUNCT_2:def 1; then
Fai in PFuncs(the carrier of [:E,F:],the carrier of F)
by A56,PARTFUN1:def 3; then
reconsider Fai as PartFunc of [:E,F:], F by PARTFUN1:46;
A58: for x be Point of E, y be Point of F st [x,y] in Z1
holds Fai.(x,y) = y - f2/.[x,y]
proof
let x be Point of E,
y be Point of F;
assume [x,y] in Z1; then
consider x0 be Point of E,y0 be Point of F such that
A59: [x,y] = [x0,y0] & Fai. [x,y] = y0 - f2/.[x0,y0] by A55;
thus thesis by A59,XTUPLE_0:1;
end;
A60:
for z0 being Point of [:E,F:]
for r being Real st z0 in Z1 & 0 < r holds
ex s being Real
st 0 < s
& for z1 being Point of [:E,F:]
st z1 in Z1 & ||.z1 - z0.|| < s holds
||. Fai /. z1 - Fai /. z0.|| < r
proof
let z0 be Point of [:E,F:],
r be Real;
assume
A61: z0 in Z1 & 0 < r;
reconsider w0 = z0 + e0b as Point of [:E,F:];
consider x0 be Point of E, y0 be Point of F such that
A62: z0 = [x0,y0] by PRVECT_3:18;
A63: 0 < 2 * (BLQ + 1) by XREAL_1:129;
consider ww0 be Point of [:E,F:] such that
A64: z0 = ww0 - e0b & ww0 in Z by A35,A61;
w0 = ww0 - (e0b - e0b) by A64,RLVECT_1:29
.= ww0 - 0. [:E,F:] by RLVECT_1:15
.= ww0 by RLVECT_1:13; then
consider s being Real such that
A65: 0 < s
& for w1 being Point of [:E,F:]
st w1 in Z & ||.w1 - w0.|| < s holds
||. f /. w1 - f /. w0.|| < r / (2 * (BLQ + 1))
by A3,A61,A63,A64,NFCONT_1:19,XREAL_1:139;
reconsider s1 = min(s,r/2) as Real;
A66: 0 < r/2 by A61,XREAL_1:215;
A67: s1 <= s & s1 <= r/2 by XXREAL_0:17;
take s1;
thus 0 < s1 by A65,A66,XXREAL_0:15;
thus for z1 being Point of [:E,F:]
st z1 in Z1 & ||.z1 - z0.|| < s1 holds
||. Fai /. z1 - Fai /. z0.|| < r
proof
let z1 be Point of [:E,F:];
assume
A68: z1 in Z1 & ||.z1 - z0.|| < s1;
reconsider w1 = z1 + e0b as Point of [:E,F:];
consider x1 be Point of E, y1 be Point of F such that
A69: z1 = [x1,y1] by PRVECT_3:18;
consider ww1 be Point of [:E,F:] such that
A70: z1= ww1 - e0b & ww1 in Z by A35,A68;
A71: w1 = ww1 - (e0b - e0b) by A70,RLVECT_1:29
.= ww1 - 0. [:E,F:] by RLVECT_1:15
.= ww1 by RLVECT_1:13;
w1 - w0 = z1 + e0b - e0b - z0 by RLVECT_1:27
.= z1 - z0 by RLVECT_4:1; then
A72: ||.w1 - w0.|| < s by A67,A68,XXREAL_0:2;
A73: Fai /. z1 = Fai.(x1,y1) by A57,A68,A69,PARTFUN1:def 6
.= y1 - f2 /. [x1,y1] by A58,A68,A69;
Fai /. z0 = Fai.(x0,y0) by A57,A61,A62,PARTFUN1:def 6
.= y0 - f2 /. [x0,y0] by A58,A61,A62; then
Fai /. z1 - Fai /. z0
= y1 - f2 /. [x1,y1] - y0 + f2 /. [x0,y0] by A73,RLVECT_1:29
.= y1 - (f2 /. [x1,y1] + y0) + f2 /. [x0,y0] by RLVECT_1:27
.= y1 - y0 - f2 /. [x1,y1] + f2 /. [x0,y0] by RLVECT_1:27
.= y1 - y0 - ( f2 /. [x1,y1] - f2 /. [x0,y0])
by RLVECT_1:29; then
A75: ||. Fai /. z1 - Fai /. z0.||
<= ||.y1-y0.|| + ||. f2/.[x1,y1] - f2/.[x0,y0] .||
by NORMSP_1:3;
A76: f2/.[x1,y1] = f2.(x1,y1) by A50,A68,A69,PARTFUN1:def 6
.= Q.(f1.(x1,y1)) by A51,A68,A69;
A77: f2/.[x0,y0] = f2.(x0,y0) by A50,A61,A62,PARTFUN1:def 6
.= Q.(f1.(x0,y0)) by A51,A61,A62;
[x1,y1+b] = [x1+ 0.E,y1+b] by RLVECT_1:4
.= w1 by A69,PRVECT_3:18; then
A79: f1.(x1,y1) = f/.w1 - c by A42,A68,A69;
[x0,y0+b] = [x0 + 0.E, y0 + b] by RLVECT_1:4
.= w0 by A62,PRVECT_3:18; then
A81: f1.(x0,y0) = f/.w0 - c by A42,A61,A62;
A82: (f/.w1 - c) - (f/.w0 - c)
= f/.w1 - c -f/.w0 + c by RLVECT_1:29
.= f/.w1 - (c + f/.w0) + c by RLVECT_1:27
.= f/.w1 - f/.w0 - c + c by RLVECT_1:27
.= f/.w1 - f/.w0 - (c - c) by RLVECT_1:29
.= f/.w1 - f/.w0 - 0. G by RLVECT_1:15
.= f/.w1 - f/.w0 by RLVECT_1:13;
A83: QQ is additive;
A84: f2/.[x1,y1] - f2/.[x0,y0]
= Q.(f/.w1 - c ) + (-1) * Q.(f/.w0 - c)
by A76,A77,A79,A81,RLVECT_1:16
.= Q.(f/.w1 - c ) + Q.((-1) * (f/.w0 - c)) by LOPBAN_1:def 5
.= Q.((f/.w1 - c) + ((-1)*(f/.w0 - c))) by A83
.= Q.(f/.w1 - f/.w0) by A82,RLVECT_1:16;
BLQ + 0 < BLQ + 1 by XREAL_1:8; then
A85: BLQ * ||.f/.w1 - f/.w0.||
<= ( BLQ + 1) * ||.f/.w1 - f/.w0.|| by XREAL_1:64;
||. Q.(f/.w1 - f/.w0) .|| <= BLQ * ||.f/.w1 - f/.w0.||
by LOPBAN_1:32; then
A86: ||. f2/.[x1,y1]-f2/.[x0,y0] .||
<= (BLQ + 1) * ||.f/.w1 - f/.w0.|| by A84,A85,XXREAL_0:2;
-z0 = [-x0,-y0] by A62,PRVECT_3:18; then
z1 - z0 = [x1 - x0,y1 - y0] by A69,PRVECT_3:18; then
||. y1-y0 .|| <= ||. z1-z0 .|| by NORMSP35; then
||. y1-y0 .|| < s1 by A68,XXREAL_0:2; then
A88: ||.y1-y0.|| < r/2 by A67,XXREAL_0:2;
(BLQ + 1) * ||.f/.w1 - f/.w0.||
< (BLQ + 1) * (r/(2*(BLQ + 1))) by A65,A70,A71,A72,XREAL_1:68; then
||. f2/.[x1,y1] - f2/.[x0,y0] .||
< (BLQ + 1) * (r/(2*(BLQ + 1))) by A86,XXREAL_0:2; then
||. f2/.[x1,y1] - f2/.[x0,y0] .|| < r/2 by XCMPLX_1:92; then
||. y1-y0 .|| + ||. f2/.[x1,y1] - f2/.[x0,y0] .|| < r/2 + r/2
by A88,XREAL_1:8;
hence ||. Fai /. z1 - Fai /. z0.|| < r by A75,XXREAL_0:2;
end;
end;
A89: for w0 being Point of [:E,F:] st w0 in Z holds
f * (reproj2 w0) is_differentiable_in w0`2
proof
let w0 be Point of [:E,F:];
assume w0 in Z; then
f is_partial_differentiable_in`2 w0 by A2,A4;
hence f * (reproj2 w0) is_differentiable_in w0 `2;
end;
A90: for w0 being Point of [:E,F:] st w0 in Z holds
ex N being Neighbourhood of w0 `2
st N c= dom (f*(reproj2 w0))
& ex R be RestFunc of F,G
st for w1 be Point of F st w1 in N holds
(f * (reproj2 w0)) /. w1 - (f*(reproj2 w0))/.(w0 `2)
= diff(f * (reproj2 w0), w0`2).(w1 - w0 `2) + R/.(w1 - w0 `2)
proof
let w0 be Point of [:E,F:];
assume w0 in Z; then
f * (reproj2 w0) is_differentiable_in w0`2 by A89;
hence thesis by NDIFF_1:def 7;
end;
A91: for z0 being Point of [:E,F:] st z0 in Z1 holds
Fai * (reproj2 z0) is_differentiable_in z0`2
& ex L0,I be Point of R_NormSpace_of_BoundedLinearOperators (F,F)
st L0 = Q * ((f `partial`2| Z) /. (z0 + e0b))
& I = id (the carrier of F)
& diff(Fai * (reproj2 z0), z0`2) = I - L0
proof
let z0 be Point of [:E,F:];
assume
A92: z0 in Z1;
reconsider w0 = z0 + e0b as Point of [:E,F:];
consider x0 be Point of E, y0 be Point of F such that
A93: z0 = [x0,y0] by PRVECT_3:18;
consider ww0 be Point of [:E,F:] such that
A94: z0= ww0 - e0b & ww0 in Z by A35,A92;
A95: w0 = ww0 - (e0b - e0b) by A94,RLVECT_1:29
.= ww0 - 0. [:E,F:] by RLVECT_1:15
.= ww0 by RLVECT_1:13; then
consider N being Neighbourhood of w0 `2 such that
A96: N c= dom(f * (reproj2 w0))
& ex R be RestFunc of F,G
st for w1 be Point of F st w1 in N holds
(f * (reproj2 w0)) /. w1 - (f * (reproj2 w0)) /. (w0 `2)
= diff(f * (reproj2 w0), w0`2).(w1 - w0 `2) + R/.(w1 - w0 `2)
by A90,A94;
consider R be RestFunc of F,G such that
A97: for w1 be Point of F st w1 in N holds
(f * (reproj2 w0)) /. w1 - (f * (reproj2 w0)) /. (w0 `2)
= diff(f * (reproj2 w0), w0`2).(w1 - w0 `2)
+ R /. (w1 - w0 `2) by A96;
reconsider L0 = Q * ((f `partial`2| Z)/.(z0+e0b))
as Point of R_NormSpace_of_BoundedLinearOperators (F,F);
id the carrier of F is Lipschitzian LinearOperator of F,F by LOPBAN_2:3;
then reconsider I = id (the carrier of F)
as Point of R_NormSpace_of_BoundedLinearOperators (F,F)
by LOPBAN_1:def 9;
reconsider L1 = I - L0 as Point of
R_NormSpace_of_BoundedLinearOperators (F,F);
reconsider R0 = Q*R as RestFunc of F,F by NDIFF_2:9;
reconsider R1 =(-1)(#)R0 as RestFunc of F,F by NDIFF_1:29;
A98: w0 = [x0+0.E, y0+b] by A93,PRVECT_3:18
.= [x0, y0+b] by RLVECT_1:4; then
A99: w0`1 = x0 & w0`2 = y0+b;
A100: z0`1 = x0 & z0`2 = y0 by A93;
set N1 = { z-b where z is Point of F : z in N };
N1 is Neighbourhood of y0+b - b by A98,NEIB1; then
reconsider N1 as Neighbourhood of y0 by RLVECT_4:1;
A101: now
let yy1 be object;
assume
A102: yy1 in N1; then
reconsider y1 = yy1 as Point of F;
A103: (reproj2 z0).y1 = [x0,y1] by A100,NDIFF_7:def 2;
consider w be Point of F such that
A104: y1 = w-b & w in N by A102;
(reproj2 w0).w in dom f by A96,A104,FUNCT_1:11; then
A105: [w0`1,w] in dom f by NDIFF_7:def 2;
reconsider x0w = [x0,w] as Point of [:E,F:];
A106: -e0b = [-0.E,-b] by PRVECT_3:18;
[x0,w-b] = [x0-0.E,w-b] by RLVECT_1:13
.= x0w -e0b by A106,PRVECT_3:18; then
A107: [x0,w-b] in Z1 by A2,A35,A98,A105;
dom(reproj2 z0) = the carrier of F by FUNCT_2:def 1;
hence yy1 in dom (Fai * (reproj2 z0)) by A57,A103,A104,A107,FUNCT_1:11;
end; then
A108: N1 c= dom (Fai * (reproj2 z0)) by TARSKI:def 3;
A109: now let y1 be Point of F;
assume
A110: y1 in N1;
A111: (reproj2 z0).y1 = [x0,y1] by A100,NDIFF_7:def 2;
consider w be Point of F such that
A112: y1 = w-b & w in N by A110;
(reproj2 w0).w in dom f by A96,A112,FUNCT_1:11; then
A113: [w0`1,w] in dom f by NDIFF_7:def 2;
reconsider x0w = [x0,w] as Point of [:E,F:];
A114: -e0b = [-0.E,-b] by PRVECT_3:18;
[x0,w-b] = [x0 - 0.E, w - b] by RLVECT_1:13
.= x0w - e0b by A114,PRVECT_3:18; then
A115: [x0,w-b] in Z1 by A2,A35,A98,A113;
dom(reproj2 z0) = the carrier of F by FUNCT_2:def 1; then
A116: y1 in dom (Fai * (reproj2 z0)) by A57,A111,A112,A115,FUNCT_1:11;
A117: (Fai * (reproj2 z0)) /. y1
= (Fai * (reproj2 z0)) . y1 by A116,PARTFUN1:def 6
.= Fai . (x0,y1) by A111,A116,FUNCT_1:12
.= y1 - f2/.[x0,y1] by A58,A112,A115;
A118: f2/.[x0,y1] = f2.(x0,y1) by A50,A112,A115,PARTFUN1:def 6
.= Q.(f1.(x0,y1)) by A51,A112,A115;
A119: [x0,y1+b] = [x0,w] by A112,RLVECT_4:1;
A120: [x0,w] = (reproj2 w0).w by A99,NDIFF_7:def 2;
A121: (f * (reproj2 w0)) /. w
= (f * (reproj2 w0)).w by A96,A112,PARTFUN1:def 6
.= f . [x0,y1+b] by A96,A112,A119,A120,FUNCT_1:12
.= f/.[x0,y1+b] by A98,A113,A119,PARTFUN1:def 6;
A122: f1.(x0,y1) = (f*(reproj2 w0))/.w - c by A42,A112,A115,A121;
A123: (reproj2 z0).y0 = [x0,y0] by A100,NDIFF_7:def 2;
A124: y0+b in N by A98,NFCONT_1:4;
(reproj2 w0).(y0+b) in dom f by A96,A124,FUNCT_1:11; then
A125: [w0`1, y0+b] in dom f by NDIFF_7:def 2;
reconsider x0v = [x0,y0+b] as Point of [:E,F:];
dom(reproj2 z0) = the carrier of F by FUNCT_2:def 1; then
A126: y0 in dom (Fai * (reproj2 z0)) by A57,A92,A93,A123,FUNCT_1:11;
then
A127: (Fai * (reproj2 z0))/.y0
= (Fai * (reproj2 z0)).y0 by PARTFUN1:def 6
.= Fai . (x0,y0) by A123,A126,FUNCT_1:12
.= y0 - f2/.[x0,y0] by A58,A92,A93;
A128: f2/.[x0,y0] = f2.(x0,y0) by A50,A92,A93,PARTFUN1:def 6
.= Q.(f1.(x0,y0)) by A51,A92,A93;
A129: [x0,y0+b] = (reproj2 w0).(y0+b) by A99,NDIFF_7:def 2;
A130: (f * (reproj2 w0))/.(y0 + b)
= (f * (reproj2 w0)).(y0 + b) by A96,A124,PARTFUN1:def 6
.= f . [x0, y0 + b] by A96,A124,A129,FUNCT_1:12
.= f/.[x0, y0 + b] by A98,A125,PARTFUN1:def 6;
A131: f1.(x0, y0)
= (f * (reproj2 w0)) /. (w0 `2) - c by A42,A92,A93,A98,A130;
A132: f1/.[x0,y1] = f1 . (x0,y1) by A41,A112,A115,PARTFUN1:def 6;
A133: f1/.[x0,y0] = f1 . (x0,y0) by A41,A92,A93,PARTFUN1:def 6;
A134: QQ is additive;
A135: f2/.[x0,y1] - f2/.[x0,y0]
= Q.(f1/.[x0,y1]) + (-1) * Q.(f1/.[x0,y0])
by A118,A128,A132,A133,RLVECT_1:16
.= Q.(f1/.[x0,y1]) + Q.((-1) * f1/.[x0,y0]) by LOPBAN_1:def 5
.= Q.(f1/.[x0,y1] + ((-1) * f1/.[x0,y0])) by A134
.= Q.(f1/.[x0,y1] - f1/.[x0,y0]) by RLVECT_1:16;
A136: w - w0 `2 = y1-y0 by A98,A112,RLVECT_1:27;
f1/.[x0,y1] - f1/.[x0,y0]
= (f * (reproj2 w0)) /. w - c - (f * (reproj2 w0)) /. w0 `2 + c
by A122,A131,A132,A133,RLVECT_1:29
.= (f * (reproj2 w0)) /. w - (c + (f * (reproj2 w0)) /. w0 `2) + c
by RLVECT_1:27
.= (f * (reproj2 w0)) /. w - (f * (reproj2 w0)) /. w0 `2 - c + c
by RLVECT_1:27
.= (f * (reproj2 w0)) /. w - (f * (reproj2 w0)) /. w0 `2
by RLVECT_4:1
.= diff(f * (reproj2 w0), (y0+b)).(y1-y0) + R/.(y1-y0)
by A97,A98,A112,A136; then
A137: f2/.[x0,y1] - f2/.[x0,y0]
= Q.(diff(f*(reproj2 w0), (y0+b)).(y1-y0)) + Q.(R/.(y1-y0))
by A134,A135;
A138: diff(f*(reproj2 w0), (y0+b))
= partdiff`2(f,w0) by A99,NDIFF_7:def 7
.= ((f `partial`2| Z)/.(z0+e0b)) by A4,A94,A95,NDIFF_7:def 11;
set Q1 = modetrans(Q,G,F);
set df1 = modetrans(diff(f*(reproj2 w0),(y0+b)),F,G);
A139: Q1 * df1 is Lipschitzian LinearOperator of F,F by LOPBAN_2:2;
A140: Q.(diff(f*(reproj2 w0),(y0+b)).(y1-y0))
= Q.(df1.(y1-y0)) by LOPBAN_1:def 11
.= Q1.(df1.(y1-y0)) by LOPBAN_1:def 11
.= (Q * ( (f `partial`2| Z)/.(z0+e0b) ) ).(y1-y0)
by A138,A139,LPB2Th4;
R is total by NDIFF_1:def 5; then
A141: dom R = the carrier of F by PARTFUN1:def 2;
rng R c= the carrier of G; then
rng R c= dom Q by FUNCT_2:def 1; then
A142: dom (Q*R) = dom R by RELAT_1:27;
A143: dom ((-1)(#) (QQ*R))
= the carrier of F by A141,A142,VFUNCT_1:def 4;
A144: Q.(R/.(y1-y0)) = Q.(R.(y1-y0)) by A141,PARTFUN1:def 6
.= (Q*R).(y1-y0) by A141,FUNCT_1:13
.= (QQ*R)/.(y1-y0) by A141,A142,PARTFUN1:def 6;
(Fai * (reproj2 z0)) /. y1 - (Fai * (reproj2 z0)) /. y0
= (y1 - f2/.[x0,y1] - y0) + f2/.[x0,y0] by A117,A127,RLVECT_1:29
.= y1 - (f2/.[x0,y1] + y0) + f2/.[x0,y0] by RLVECT_1:27
.= y1 - y0 - f2/.[x0,y1] + f2/.[x0,y0] by RLVECT_1:27
.= y1 - y0 - (L0.(y1-y0) + R0/.(y1-y0)) by A137,A140,A144,RLVECT_1:29
.= y1 - y0 - L0.(y1-y0) - R0/.(y1-y0) by RLVECT_1:27
.= y1 - y0 + -L0.(y1-y0) +(-1) * R0/.(y1-y0) by RLVECT_1:16
.= I.(y1-y0) - L0.(y1-y0) +((-1)(#)R0 )/.(y1-y0)
by A143,VFUNCT_1:def 4
.= L1.(y1-y0)+ R1/.(y1-y0) by LOPBAN_1:40;
hence (Fai * (reproj2 z0)) /. y1 - (Fai * (reproj2 z0)) /.z0 `2
= L1 . (y1 - z0 `2) + R1 /. (y1 - z0 `2) by A93;
end;
hence
A145: Fai * (reproj2 z0) is_differentiable_in z0 `2
by A93,A101,NDIFF_1:def 6,TARSKI:def 3;
take L0,I;
thus L0 = Q * ((f `partial`2|Z)/.(z0+e0b))
& I = id (the carrier of F)
& diff(Fai*(reproj2 z0),z0`2) = I-L0
by A93,A108,A109,A145,NDIFF_1:def 7;
end;
for z0 being Point of [:E,F:] st z0 in Z1 holds
Fai is_partial_differentiable_in`2 z0 by A91; then
A146: Fai is_partial_differentiable_on`2 Z1 by FUNCT_2:def 1;
A147: dom (Fai `partial`2|Z1) = Z1
& for z be Point of [:E,F:] st z in Z1 holds
ex L,I be Point of R_NormSpace_of_BoundedLinearOperators (F,F)
st L = Q * ((f `partial`2| Z)/.(z + e0b))
& I = id (the carrier of F)
& (Fai `partial`2| Z1)/.z = I - L
proof
thus dom (Fai `partial`2| Z1) = Z1 by A146,NDIFF_7:def 11;
let z be Point of [:E,F:];
assume
A148: z in Z1; then
consider L,I be Point of R_NormSpace_of_BoundedLinearOperators (F,F)
such that
A149: L = Q * ((f `partial`2| Z)/.(z + e0b))
& I = id (the carrier of F)
& diff(Fai * (reproj2 z), z`2) = I - L by A91;
take L,I;
thus L = Q * ((f `partial`2| Z)/.(z + e0b))
& I = id (the carrier of F) by A149;
thus (Fai `partial`2| Z1)/.z
= partdiff`2 (Fai,z) by A146,A148,NDIFF_7:def 11
.= I - L by A149,NDIFF_7:def 7;
end;
set FG = Fai `partial`2| Z1;
A150:
for z0 being Point of [:E,F:]
for r being Real st z0 in Z1 & 0 < r holds
ex s being Real
st 0 < s
& for z1 being Point of [:E,F:]
st z1 in Z1 & ||.z1 - z0.|| < s holds
||. FG /. z1 - FG /. z0.|| < r
proof
let z0 be Point of [:E,F:],
r be Real;
reconsider w0 = z0 + e0b as Point of [:E,F:];
assume
A151: z0 in Z1 & 0 < r; then
consider ww0 be Point of [:E,F:] such that
A152: z0 = ww0 - e0b & ww0 in Z by A35;
w0 = ww0 -(e0b - e0b ) by A152,RLVECT_1:29
.= ww0 - 0. [:E,F:] by RLVECT_1:15
.= ww0 by RLVECT_1:13; then
consider s being Real such that
A153: 0 < s
& for w1 being Point of [:E,F:]
st w1 in Z & ||.w1 - w0.|| < s holds
||. (f `partial`2| Z) /. w1 - (f `partial`2| Z ) /. w0.||
< r / (BLQ + 1) by A5,A151,A152,NFCONT_1:19,XREAL_1:139;
take s;
thus 0 < s by A153;
thus for z1 being Point of [:E,F:]
st z1 in Z1 & ||.z1 - z0.|| < s
holds ||. FG /. z1 - FG /. z0.|| < r
proof
let z1 be Point of [:E,F:];
reconsider w1 = z1 + e0b as Point of [:E,F:];
assume
A154: z1 in Z1 & ||.z1 - z0.|| < s; then
consider ww1 be Point of [:E,F:] such that
A155: z1 = ww1 - e0b & ww1 in Z by A35;
A156: w1 = ww1 -(e0b - e0b ) by A155,RLVECT_1:29
.= ww1 - 0. [:E,F:] by RLVECT_1:15
.= ww1 by RLVECT_1:13;
A157: w1 - w0 = z1 + e0b - e0b - z0 by RLVECT_1:27
.= z1 - z0 by RLVECT_4:1;
consider Lz0,Iz0 be Point of
R_NormSpace_of_BoundedLinearOperators (F,F) such that
A158: Lz0 = Q * ((f `partial`2| Z)/.(z0 + e0b))
& Iz0 = id (the carrier of F)
& (Fai `partial`2| Z1) /. z0 = Iz0 -Lz0 by A147,A151;
consider Lz1,Iz1 be Point of
R_NormSpace_of_BoundedLinearOperators (F,F) such that
A159: Lz1 = Q * ((f `partial`2| Z)/.(z1 + e0b))
& Iz1 = id (the carrier of F)
& (Fai `partial`2| Z1)/.z1 = Iz1 - Lz1 by A147,A154;
FG /. z1 - FG /. z0
= Iz1 - Lz1 - Iz0 + Lz0 by A158,A159,RLVECT_1:29
.= Iz1 - (Iz0 + Lz1) + Lz0 by RLVECT_1:27
.= Iz1 - Iz0 - Lz1 + Lz0 by RLVECT_1:27
.= Iz1 - Iz0 - ( Lz1 - Lz0 ) by RLVECT_1:29
.= 0.R_NormSpace_of_BoundedLinearOperators(F,F)
- ( Lz1 - Lz0 ) by A158,A159,RLVECT_1:15
.= - ( Lz1 - Lz0 ) by RLVECT_1:14; then
A160: ||. FG /. z1 - FG /. z0.||
= ||.Lz1 - Lz0 .|| by NORMSP_1:2;
BLQ + 0 < BLQ + 1 by XREAL_1:8; then
A161: BLQ * ||.(f `partial`2| Z)/.w1 - (f `partial`2| Z)/.w0 .||
<= (BLQ + 1) * ||.(f `partial`2| Z)/.w1 - (f `partial`2| Z)/.w0 .||
by XREAL_1:64;
A162: Q*((-1)* ((f `partial`2| Z)/.w0) )
= (1*Q)*((-1)* ((f `partial`2| Z)/.w0)) by RLVECT_1:def 8
.= (1*(-1))*(Q*((f `partial`2|Z)/.w0 )) by LPB2Th11
.= - Q*( (f `partial`2|Z)/.w0 ) by RLVECT_1:16;
A163: Q*( (f `partial`2|Z)/.w1 )-Q*((f `partial`2|Z)/.w0 )
= Q*( (f `partial`2|Z)/.w1 + (-1)* ((f `partial`2|Z)/.w0))
by A162,LPB2Th9
.= Q*( (f `partial`2|Z)/.w1 -(f `partial`2|Z)/.w0) by RLVECT_1:16;
set Q1 = modetrans(Q,G,F);
set fp10= modetrans((f `partial`2|Z)/.w1 - (f `partial`2|Z)/.w0,F,G);
A164: (BoundedLinearOperatorsNorm(G,F).Q1) = BLQ by LOPBAN_1:def 11;
||. Lz1 - Lz0 .||
<= (BoundedLinearOperatorsNorm(G,F).Q1)
* (BoundedLinearOperatorsNorm(F,G).fp10)
by A158,A159,A163,LOPBAN_2:2; then
||. Lz1 - Lz0 .||
<= BLQ * ||.(f `partial`2|Z)/.w1 - (f `partial`2|Z)/.w0.||
by A164,LOPBAN_1:def 11; then
A165: ||. Lz1 - Lz0 .||
<= (BLQ + 1) * ||.(f `partial`2| Z)/.w1 - (f `partial`2| Z)/.w0.||
by A161,XXREAL_0:2;
(BLQ + 1) * ||.(f `partial`2| Z)/.w1 - (f `partial`2| Z)/.w0.||
< (BLQ + 1) * (r / (BLQ + 1)) by A153,A154,A155,A156,A157,XREAL_1:68;
then
||. Lz1 - Lz0 .|| < (BLQ + 1) * (r/(BLQ + 1)) by A165,XXREAL_0:2;
hence ||. FG /. z1 - FG /. z0.|| < r by A160,XCMPLX_1:87;
end;
end;
A166: [a,0.F + b] in Z by A6,RLVECT_1:def 4; then
A167: [a,0.F] in Z1 by A21;
A169: Fai.(a,0.F) = 0.F - f2/.[a,0.F] by A21,A58,A166;
A168: Fai.(a,0.F) = 0.F
proof
f2/.[a,0.F] = f2.(a,0.F) by A21,A50,A166,PARTFUN1:def 6
.= Q.(f1.(a,0.F)) by A21,A51,A166
.= Q.(f/.[a,0.F+b] - c) by A21,A42,A166
.= Q.( f/.[a,b] - c ) by RLVECT_1:def 4
.= Q.( c - c ) by A2,A6,A7,PARTFUN1:def 6
.= Q. 0.G by RLVECT_1:15
.= 0.F by LOPBAN_7:3;
hence thesis by A169,RLVECT_1:15;
end;
reconsider a0F = [a,0.F] as Point of [:E,F:];
consider r10 being Real such that
A170: 0 < r10
& for s being Point of [:E,F:] st s in Z1 & ||.s - a0F.|| < r10 holds
||. (Fai `partial`2|Z1)/.s - (Fai `partial`2|Z1)/.a0F .|| < 1/4
by A21,A150,A166;
consider r11 being Real such that
A171: 0 < r11 & Ball(a0F,r11) c= Z1 by A21,A36,A166,NORMSP27;
reconsider r12 = min(r10,r11) as Real;
A173: r12 <= r11 & r12 <= r10 by XXREAL_0:17; then
A174: Ball(a0F,r12) c= Ball(a0F,r11) by LMBALL1;
0 < r12 by A170,A171,XXREAL_0:15; then
consider r1 be Real such that
A175: 0 < r1 & r1 < r12
& [: Ball(a,r1),Ball(0.F,r1):] c= Ball(a0F,r12) by NORMSP31;
[: Ball(a,r1),Ball(0.F,r1):]
c= Ball(a0F,r11) by A174,A175,XBOOLE_1:1; then
A176: [: Ball(a,r1),Ball(0.F,r1):] c= Z1 by A171,XBOOLE_1:1;
A177: for x being Point of [:E,F:] st x in Z1 holds
(Fai `partial`2|Z1)/.x = diff((Fai * (reproj2 x)), (x `2))
proof
let x be Point of [:E,F:];
assume x in Z1;
hence (Fai `partial`2|Z1)/.x
= partdiff`2 (Fai,x) by A146,NDIFF_7:def 11
.= diff((Fai * (reproj2 x)), (x `2)) by NDIFF_7:def 7;
end;
A179: a in Ball(a,r1) by A175,LMBALL2;
0.F in Ball(0.F,r1) by A175,LMBALL2; then
A181: [a,0.F] in [:Ball(a,r1),Ball(0.F,r1):] by A179,ZFMISC_1:87;
reconsider a0F = [a,0.F] as Point of [:E,F:];
consider La0f,Ia0f be Point of R_NormSpace_of_BoundedLinearOperators(F,F)
such that
A182: La0f = Q * ((f `partial`2| Z) /. (a0F + e0b))
& Ia0f = id (the carrier of F)
& (Fai `partial`2| Z1) /. a0F
= Ia0f - La0f by A147,A176,A181;
partdiff`2(f,z) is Lipschitzian LinearOperator of F,G by LOPBAN_1:def 9;
then
A183: dom( partdiff`2(f,z) ) = the carrier of F by FUNCT_2:def 1;
A184: Q = modetrans((partdiff`2(f,z))",G,F) by A10,LOPBAN_1:def 11;
A185: partdiff`2(f,z) = modetrans(partdiff`2(f,z),F,G) by LOPBAN_1:def 11;
a0F + e0b = [a+0.E, 0.F+b] by PRVECT_3:18
.= [a, 0.F+b] by RLVECT_1:4
.= z by A6,RLVECT_1:4; then
A186: La0f = Q * (partdiff`2(f,z)) by A4,A6,A182,NDIFF_7:def 11
.= Ia0f by A8,A10,A182,A183,A184,A185,FUNCT_1:39;
A187: (Fai `partial`2| Z1) /. [a,0.F]
= 0.(R_NormSpace_of_BoundedLinearOperators(F,F)) by A182,A186,RLVECT_1:15;
A188: for x be Point of E, y be Point of F
st x in Ball(a,r1) & y in Ball(0.F,r1)
holds ||. (Fai `partial`2|Z1)/.[x,y] .|| < 1/4
proof
let x be Point of E, y be Point of F;
assume x in Ball(a,r1) & y in Ball(0.F,r1); then
A190: [x,y] in [:Ball(a,r1),Ball(0.F,r1):] by ZFMISC_1:87;
reconsider s = [x,y] as Point of [:E,F:];
s in Ball(a0F,r12) by A175,A190; then
ex q be Element of [:E,F:] st s = q & ||.a0F-q.|| < r12; then
||.s-a0F.|| < r12 by NORMSP_1:7; then
||.s-a0F.|| < r10 by A173,XXREAL_0:2; then
||. (Fai `partial`2|Z1)/.s - (Fai `partial`2|Z1)/.a0F .|| < 1/4
by A170,A176,A190;
hence thesis by A187,RLVECT_1:13;
end;
reconsider r2 = r1/2 as Real;
0 < 1/2 & 0 < r1/2 by A175,XREAL_1:215; then
consider ar10 being Real such that
A191: 0 < ar10
& for s being Point of [:E,F:] st s in Z1 & ||.s - a0F.|| < ar10
holds ||. Fai/.s - Fai/.a0F .|| < (1/2) * r2
by A60,A167,XREAL_1:129;
consider ar12 be Real such that
A192: 0 < ar12 & ar12 < ar10
& [:Ball(a,ar12),Ball(0.F,ar12):] c= Ball(a0F,ar10)
by A191,NORMSP31;
reconsider ar11 = min(ar10,ar12) as Real;
A193: 0 < ar11 by A192,XXREAL_0:21;
ar11 <= ar10 & ar11 <= ar12 by XXREAL_0:17; then
A195: Ball(a,ar11) c= Ball(a,ar12) by LMBALL1;
reconsider ar1 = min(ar11,r1) as Real;
A196: 0 < ar1 by A175,A193,XXREAL_0:21;
A197: ar1 <= ar11 & ar1 <= r1 by XXREAL_0:17; then
A198: Ball(a,ar1) c= Ball(a,r1) by LMBALL1;
A199: Ball(a,ar1) c= Ball(a,ar11) by A197,LMBALL1;
A200: for x be Point of E st x in Ball(a,ar1)
holds ||. Fai/.[x,0.F] .|| <= (1/2) * r2
proof
let x be Point of E;
assume
A201: x in Ball(a,ar1);
0.F in Ball(0.F,r1) by A175,LMBALL2; then
A202: [x,0.F] in [:Ball(a,r1),Ball(0.F,r1):]
by A198,A201,ZFMISC_1:87;
reconsider x0F = [x,0.F] as Point of [:E,F:];
A203: x in Ball(a,ar11) by A199,A201;
0.F in Ball(0.F,ar12) by A192,LMBALL2; then
[x,0.F] in [:Ball(a,ar12),Ball(0.F,ar12):] by A195,A203,ZFMISC_1:87; then
x0F in Ball(a0F,ar10) by A192; then
ex q be Element of [:E,F:]
st q = x0F & ||. a0F - q .|| < ar10; then
||. x0F - a0F .|| < ar10 by NORMSP_1:7; then
A204: ||. Fai/.x0F - Fai/.a0F .|| < (1/2) * r2 by A176,A191,A202;
Fai/.a0F = 0.F by A146,A167,A168,PARTFUN1:def 6;
hence thesis by A204,RLVECT_1:13;
end;
reconsider r0 = min(r1/2,ar1) as Real;
A205: 0 < r1/2 by A175,XREAL_1:215; then
A206: 0 < r0 by A196,XXREAL_0:21;
A207: r0 <= r1/2 by XXREAL_0:17;
r1/2 < r1 by A175,XREAL_1:216; then
r0 < r1 by A207,XXREAL_0:2; then
A208: Ball(a,r0) c= Ball(a,r1) by LMBALL1;
A209: for x be Point of E st x in Ball(a,r0)
holds ||. Fai/.[x,0.F] .|| <= (1/2) * r2
proof
let x be Point of E;
assume
A210: x in Ball(a,r0);
r0 <= ar1 by XXREAL_0:17; then
Ball(a,r0) c= Ball(a,ar1) by LMBALL1;
hence ||. Fai/.[x,0.F] .|| <= (1/2)*r2 by A200,A210;
end;
take r0,r2;
thus 0 < r0 & 0 < r2 by A196,A205,XXREAL_0:21;
A211: cl_Ball(0.F,r2) c= Ball(0.F,r1) by A175,LMBALL1X,XREAL_1:216; then
[:Ball(a,r0),cl_Ball(0.F,r2):]
c= [:Ball(a,r1),Ball(0.F,r1):] by A208,ZFMISC_1:96; then
A212: [:Ball(a,r0),cl_Ball(0.F,r2):] c= Z1 by A176,XBOOLE_1:1;
A213: for x be Point of E st x in Ball(a,r0) holds
for y1,y2 be Point of F
st y1 in cl_Ball(0.F,r2) & y2 in cl_Ball(0.F,r2)
holds ||. Fai/.[x,y1] - Fai/.[x,y2] .|| <= (1/2) * ||. y1- y2 .||
proof
let x be Point of E;
assume
A214: x in Ball(a,r0);
let y1,y2 be Point of F;
assume that
A215: y1 in cl_Ball(0.F,r2) and
A216: y2 in cl_Ball(0.F,r2);
A217: [.y1,y2.] c= cl_Ball(0.F,r2) by A215,A216,LMCLOSE2;
A218: ].y1,y2.[ c= [.y1,y2.] by XBOOLE_1:36;
reconsider s = [x,y1] as Point of [:E,F:];
reconsider Fs = Fai * (reproj2 s) as PartFunc of F,F;
A219: for y be object st y in [.y1,y2.] holds y in dom Fs
proof
let y be object;
assume
A220: y in [.y1,y2.]; then
[x,y] in [:Ball(a,r0),cl_Ball(0.F,r2):]
by A214,A217,ZFMISC_1:87; then
A221: [x,y] in Z1 by A212;
A222: y in the carrier of F by A220;
(s `1) = x; then
A223: (reproj2 s).y in Z1 by A220,A221,NDIFF_7:def 2;
y in dom (reproj2 s) by A222,FUNCT_2:def 1;
hence y in dom Fs by A146,A223,FUNCT_1:11;
end;
A224: for y being Point of F st y in [.y1,y2.]
holds Fs is_differentiable_in y
proof
let y be Point of F;
assume y in [.y1,y2.]; then
A225: [x,y] in [:Ball(a,r0),cl_Ball(0.F,r2):]
by A214,A217,ZFMISC_1:87;
reconsider s1 = [x,y] as Point of [:E,F:];
A226: Fai * (reproj2 s1) is_differentiable_in s1 `2 by A91,A212,A225;
s1`1 = s`1;
hence thesis by A226,REP2;
end;
A227: for y being Point of F st y in [.y1,y2.] holds
Fs is_continuous_in y by A224,NDIFF_1:44;
A228: for y being Point of F st y in ].y1,y2.[
holds Fs is_differentiable_in y by A218,A224;
A229: for y being Point of F st y in ].y1,y2.[ holds
||. diff (Fs,y) .|| <= 1/2
proof
let y be Point of F;
assume y in ].y1,y2.[; then
A230: y in [.y1,y2.] by A218; then
A231: y in cl_Ball(0.F,r2) by A217;
A232: [x,y] in [:Ball(a,r0),cl_Ball(0.F,r2):]
by A214,A217,A230,ZFMISC_1:87;
reconsider s1 = [x,y] as Point of [:E,F:];
||. (Fai `partial`2|Z1)/. [x,y] .|| <= 1/4
by A188,A208,A211,A214,A231; then
A233: ||. diff ((Fai * (reproj2 s1)), (s1 `2)) .|| <= 1/4
by A177,A212,A232;
s1`1 = s`1; then
Fai * (reproj2 s1) = Fs by REP2;
hence thesis by A233,XXREAL_0:2;
end;
A234: ||.(Fs /. y2) - (Fs /. y1).|| <= (1/2) * ||.y2-y1.||
by A219,A227,A228,A229,NDIFF_5:19,TARSKI:def 3;
[x,y1] in [:Ball(a,r0),cl_Ball(0.F,r2):]
& [x,y2] in [:Ball(a,r0),cl_Ball(0.F,r2):]
by A214,A215,A216,ZFMISC_1:87; then
A237: [x,y1] in Z1 & [x,y2] in Z1 by A212;
A235: dom(reproj2 s) = the carrier of F by FUNCT_2:def 1;
A236: y1 in [.y1,y2.] & y2 in [.y1,y2.] by RLTOPSP1:68; then
A238: Fs /. y1 = (Fai * (reproj2 s)).y1 by A219,PARTFUN1:def 6
.= Fai.((reproj2 s).y1) by A235,FUNCT_1:13
.= Fai. [s`1,y1] by NDIFF_7:def 2
.= Fai/.[x,y1] by A146,A237,PARTFUN1:def 6;
A239: Fs /. y2 = (Fai * (reproj2 s)).y2
by A219,A236,PARTFUN1:def 6
.= Fai.((reproj2 s).y2) by A235,FUNCT_1:13
.= Fai. [s`1,y2] by NDIFF_7:def 2
.= Fai/.[x,y2] by A146,A237,PARTFUN1:def 6;
||.((Fs /. y2) - (Fs /. y1)).||
= ||. Fai/.[x,y1] - Fai/.[x,y2] .|| by A238,A239,NORMSP_1:7;
hence thesis by A234,NORMSP_1:7;
end;
A240: for x be Point of E, y be Point of F
st x in Ball(a,r0) & y in cl_Ball(0.F,r2)
holds Fai.(x,y) in cl_Ball(0.F,r2)
proof
let x be Point of E, y be Point of F;
assume
A241: x in Ball(a,r0) & y in cl_Ball(0.F,r2); then
[x,y] in [:Ball(a,r0),cl_Ball(0.F,r2):] by ZFMISC_1:87; then
A242: [x,y] in Z1 by A212;
A243: 0.F in cl_Ball(0.F,r2) by A205,LMBALL2;
ex p be Point of F st p = y & ||. 0.F - p .|| <= r2 by A241; then
||. y - 0.F .|| <= r2 by NORMSP_1:7; then
A244: (1/2) * ||. y - 0.F .|| <= (1/2) * r2 by XREAL_1:64;
A245: ||. Fai/.[x,0.F] .|| <= (1/2) * r2 by A209,A241;
||. Fai/.[x,y] - Fai/.[x,0.F] .||
<= (1/2) * ||. y - 0.F .|| by A213,A241,A243; then
A246: ||. Fai/.[x,y] - Fai/.[x,0.F] .||
<= (1/2) * r2 by A244,XXREAL_0:2;
A247: Fai.(x,y) = Fai/.[x,y] by A146,A242,PARTFUN1:def 6; then
reconsider Fxy = Fai.(x,y) as Point of F;
Fxy - 0.F = Fai/.[x,y] - (Fai/.[x,0.F] - Fai/.[x,0.F])
by A247,RLVECT_1:15
.= ( Fai/.[x,y] - Fai/.[x,0.F] )
+ Fai/.[x,0.F] by RLVECT_1:29; then
A248: ||. Fxy - 0.F .|| <= ||. Fai/.[x,y] - Fai/.[x,0.F] .||
+ ||. Fai/.[x,0.F] .|| by NORMSP_1:def 1;
||. Fai/.[x,y] - Fai/.[x,0.F] .|| + ||. Fai/.[x,0.F] .||
<= (1/2) * r2 + (1/2) * r2 by A245,A246,XREAL_1:7; then
||. Fxy - 0.F .|| <= r2 by A248,XXREAL_0:2; then
||. 0.F - Fxy .|| <= r2 by NORMSP_1:7;
hence Fai.(x,y) in cl_Ball(0.F,r2);
end;
A249: [:Ball(a,r0),cl_Ball(0.F,r2):] c= dom Fai by A212,FUNCT_2:def 1;
A251: Ball(a,r0) <>{} by A206,LMBALL2;
A252: cl_Ball(0.F,r2) <> {} by A205,LMBALL2;
A253:
for y be Point of F st y in cl_Ball(0.F,r2) holds
for x0 be Point of E st x0 in Ball(a,r0)
for e be Real st 0 < e
ex d be Real
st 0 < d
& for x1 be Point of E
st x1 in Ball(a,r0)
& ||.x1-x0.|| < d
holds ||. Fai/.[x1,y] - Fai/.[x0,y] .|| < e
proof
let y be Point of F;
assume
A254: y in cl_Ball(0.F,r2);
let x0 be Point of E;
assume x0 in Ball(a,r0); then
A257: [x0,y] in [:Ball(a,r0),cl_Ball(0.F,r2):] by A254,ZFMISC_1:87;
reconsider z0=[x0,y] as Point of [:E,F:];
let e be Real;
assume
A256: 0 < e;
consider s being Real such that
A258: 0 < s
& for z1 being Point of [:E,F:]
st z1 in Z1 & ||.z1 - z0.|| < s holds
||. Fai /. z1 - Fai /. z0.|| < e by A60,A212,A256,A257;
take s;
thus 0 < s by A258;
let x1 be Point of E;
assume
A259: x1 in Ball(a,r0) & ||.x1-x0.|| < s; then
A260: [x1,y] in [:Ball(a,r0),cl_Ball(0.F,r2):] by A254,ZFMISC_1:87;
reconsider z1 = [x1,y] as Point of [:E,F:];
-z0 = [-x0,-y] by PRVECT_3:18; then
z1 - z0 = [x1-x0,y-y] by PRVECT_3:18
.= [x1-x0,0.F] by RLVECT_1:15;
then ||.z1 - z0.|| = ||.x1-x0.|| by LMNR1;
hence ||. Fai/.[x1,y] - Fai/.[x0,y] .|| < e by A212,A258,A259,A260;
end; then
consider Psi be PartFunc of E,F such that
A262: Psi is_continuous_on Ball(a,r0)
& dom Psi = Ball(a,r0)
& rng Psi c= cl_Ball(0.F,r2)
& for x be Point of E st x in Ball(a,r0)
holds Fai.(x,Psi.x) = Psi.x
by A213,A240,A249,A251,A252,FIXPOINT3;
for z be object holds z in cl_Ball(b,r2) iff
z in {y+b where y is Point of F : y in cl_Ball(0.F,r2) }
proof
let z be object;
hereby
assume z in cl_Ball(b,r2); then
consider p be Point of F such that
A263: p = z & ||. b-p .|| <= r2;
reconsider y = p-b as Point of F;
A264: y + b = p - (b-b) by RLVECT_1:29
.= p - 0.F by RLVECT_1:15
.= p by RLVECT_1:13;
||. 0.F - y .|| = ||. y - 0.F .|| by NORMSP_1:7
.= ||.y.|| by RLVECT_1:13; then
||. 0.F - y .|| <= r2 by A263,NORMSP_1:7; then
y in cl_Ball(0.F,r2);
hence z in {y+b where y is Point of F : y in cl_Ball(0.F,r2)}
by A263,A264;
end;
assume z in {y+b where y is Point of F : y in cl_Ball(0.F,r2)}; then
consider y be Point of F such that
A265: z = y+b & y in cl_Ball(0.F,r2);
A266: ||. ( y+b ) - b .|| = ||. y + (b-b) .|| by RLVECT_1:28
.= ||. y + 0.F .|| by RLVECT_1:15
.= ||.y.|| by RLVECT_1:4;
ex p be Point of F st p=y & ||.0.F -p .|| <= r2 by A265; then
||. y -0.F .|| <= r2 by NORMSP_1:7; then
||. ( y+b ) - b .|| <= r2 by A266,RLVECT_1:13; then
||. b - ( y+b ) .|| <= r2 by NORMSP_1:7;
hence z in cl_Ball(b,r2) by A265;
end; then
A267: cl_Ball(b,r2)
= {y+b where y is Point of F : y in cl_Ball(0.F,r2)} by TARSKI:2;
A268: K.:[:Ball(a,r0),cl_Ball(0.F,r2):]
c= K.:Z1 by A212,RELAT_1:123;
A269: K.:Z1 = H"(H.:Z) by A19,A20,FUNCT_1:85
.= Z by A15,A19,FUNCT_1:94;
for y being object holds
(y in [:Ball(a,r0),cl_Ball(b,r2):]
iff
ex x being object
st x in dom K & x in [:Ball(a,r0),cl_Ball(0.F,r2):] & y = K.x)
proof
let y be object;
hereby
assume y in [:Ball(a,r0),cl_Ball(b,r2):]; then
consider d,w be object such that
A270: d in Ball(a,r0) & w in cl_Ball(b,r2) & y = [d,w]
by ZFMISC_1:def 2;
reconsider d as Point of E by A270;
reconsider w as Point of F by A270;
reconsider b2 = w-b as Point of F;
reconsider p=[d,b2] as Point of [:E,F:];
consider y0 be Point of F such that
A271: w = y0+b & y0 in cl_Ball(0.F,r2) by A267,A270;
A272: w-b = y0+(b-b) by A271,RLVECT_1:28
.= y0 + 0.F by RLVECT_1:15
.= y0 by RLVECT_1:def 4; then
y = [d+0.E,b2+b] by A270,A271,RLVECT_1:def 4
.= p + e0b by PRVECT_3:18
.= 1 * p + e0b by RLVECT_1:def 8
.= K.p by A16;
hence ex x being object st
x in dom K & x in [:Ball(a,r0),cl_Ball(0.F,r2):] &
y = K . x by A17,A270,A271,A272,ZFMISC_1:87;
end;
given x being object such that
A273: x in dom K & x in [:Ball(a,r0),cl_Ball(0.F,r2):] & y = K . x;
reconsider p = x as Point of [:E,F:] by A273;
A274: K.x = 1 * p + e0b by A16
.= p + e0b by RLVECT_1:def 8;
consider z be Point of E,w be Point of F such that
A275: p = [z,w] by PRVECT_3:18;
A276: p + e0b = [z+0.E,w+b] by A275,PRVECT_3:18
.= [z,w+b] by RLVECT_1:def 4;
A277: z in Ball(a,r0) & w in cl_Ball(0.F,r2)
by A273,A275,ZFMISC_1:87; then
w + b in cl_Ball(b,r2) by A267;
hence y in [:Ball(a,r0),cl_Ball(b,r2):]
by A273,A274,A276,A277,ZFMISC_1:87;
end;
hence [:Ball(a,r0),cl_Ball(b,r2):] c= Z by A268,A269,FUNCT_1:def 6;
deffunc FX11(object) = Psi/.$1 + b;
A278: for y being object st y in Ball(a,r0) holds
FX11(y) in cl_Ball(b,r2)
proof
let y be object such that
A279: y in Ball(a,r0);
reconsider yp = y as Point of E by A279;
Psi.yp in rng Psi by A262,A279,FUNCT_1:3; then
Psi.yp in cl_Ball(0.F,r2) by A262; then
Psi/.yp in cl_Ball(0.F,r2) by A262,A279,PARTFUN1:def 6;
hence FX11(y) in cl_Ball(b,r2) by A267;
end;
consider Eta being Function of Ball(a,r0),cl_Ball(b,r2) such that
A280: for y being object st y in Ball(a,r0) holds
Eta . y = FX11(y) from FUNCT_2:sch 2(A278);
A281: rng Eta c= cl_Ball(b,r2);
cl_Ball(b,r2) <> {} by A205,LMBALL2; then
A282: dom Eta = Ball(a,r0) by FUNCT_2:def 1;
rng Eta c= the carrier of F by XBOOLE_1:1; then
reconsider Eta as PartFunc of E,F by A282,RELSET_1:4;
A284:for x0 being Point of E
for r being Real
st x0 in Ball(a,r0) & 0 < r holds
ex s being Real
st 0 < s
& for x1 being Point of E
st x1 in Ball(a,r0) & ||.x1 - x0.|| < s holds
||. Eta /. x1 - Eta /. x0.|| < r
proof
let x0 be Point of E;
let r be Real;
assume
A285: x0 in Ball(a,r0) & 0 < r; then
consider s being Real such that
A286: 0 < s
& for x1 being Point of E
st x1 in Ball(a,r0) & ||.x1 - x0.|| < s
holds ||. Psi /. x1 - Psi /. x0 .|| < r by A262,NFCONT_1:19;
take s;
thus 0 < s by A286;
let x1 be Point of E;
assume
A287: x1 in Ball(a,r0) & ||.x1 - x0.|| < s; then
A288: Eta/.x1 = Eta.x1 by A282,PARTFUN1:def 6
.= Psi/.x1 + b by A280,A287;
Eta/.x0 = Eta.x0 by A282,A285,PARTFUN1:def 6
.= Psi/.x0 + b by A280,A285; then
Eta/.x1 - Eta/.x0 = (Psi/.x1 + b -b ) - Psi/.x0 by A288,RLVECT_1:27
.= Psi/.x1 - Psi/.x0 by RLVECT_4:1;
hence ||. Eta /. x1 - Eta /. x0.|| < r by A286,A287;
end;
A290: for x be Point of E st x in Ball(a,r0)
holds f.(x,Eta.x) = c
proof
let x be Point of E;
assume
A291: x in Ball(a,r0); then
A292: Psi.x in rng Psi by A262,FUNCT_1:3; then
reconsider y = Psi.x as Point of F;
A293: y in cl_Ball(0.F,r2) & Fai.(x,y) = y by A262,A291,A292;
A294: [x,y] in [:Ball(a,r0),cl_Ball(0.F,r2):]
by A262,A291,A292,ZFMISC_1:87; then
y = y - f2/.[x,y] by A58,A212,A293; then
- -f2/.[x,y] = - 0.F by RLVECT_1:9; then
f2/.[x,y] = - 0.F by RLVECT_1:17; then
A295: f2/.[x,y] = 0.F by RLVECT_1:12;
f2.(x,y) = f2/.[x,y] by A50,A212,A294,PARTFUN1:def 6; then
A296: Q.(f1.(x,y)) =0.F by A51,A212,A294,A295;
f1.(x,y) = f1/.[x,y] by A41,A212,A294,PARTFUN1:def 6; then
f1.(x,y) =0.G by A8,A10,A296,LQ2; then
0.G = f/.[x,y+b] - c by A42,A212,A294; then
A297: f/.[x,y+b] = c by RLVECT_1:21;
y + b = Psi/.x + b by A262,A291,PARTFUN1:def 6
.= Eta.x by A280,A291;
hence thesis by A2,A21,A212,A294,A297,PARTFUN1:def 6;
end;
A298: for x be Point of E st x in Ball(a,r0) holds
ex y be Point of F st y in cl_Ball(b,r2) & f.(x,y) = c
proof
let x be Point of E;
assume
A299: x in Ball(a,r0); then
A300: Eta.x in rng Eta by A282,FUNCT_1:3; then
reconsider y = Eta.x as Point of F;
take y;
thus y in cl_Ball(b,r2) by A281,A300;
thus f.(x,y) = c by A290,A299;
end;
A301:
for x be Point of E st x in Ball(a,r0) holds
(for y1,y2 be Point of F
st y1 in cl_Ball(b,r2) & y2 in cl_Ball(b,r2)
& f.(x,y1) = c & f.(x,y2) = c holds y1 = y2)
proof
let x be Point of E;
assume
A302: x in Ball(a,r0);
let y1,y2 be Point of F;
assume
A303: y1 in cl_Ball(b,r2) & y2 in cl_Ball(b,r2)
& f.(x,y1) = c & f.(x,y2) = c; then
consider y10 be Point of F such that
A304: y1 = y10 + b & y10 in cl_Ball(0.F,r2) by A267;
consider y20 be Point of F such that
A305: y2 = y20 + b & y20 in cl_Ball(0.F,r2) by A267,A303;
A306: [x,y10] in [:Ball(a,r0),cl_Ball(0.F,r2):] by A302,A304,ZFMISC_1:87;
A307: [x,y20] in [:Ball(a,r0),cl_Ball(0.F,r2):] by A302,A305,ZFMISC_1:87;
A308: [x,y10] in [:Ball(a,r0),cl_Ball(0.F,r2):] by A302,A304,ZFMISC_1:87;
A309: [x,y20] in [:Ball(a,r0),cl_Ball(0.F,r2):] by A302,A305,ZFMISC_1:87;
f.(x,y1) = f/.[x,y1] by A2,A21,A212,A304,A306,PARTFUN1:def 6; then
f/.[x,y10+b] - c = 0.G by A303,A304,RLVECT_1:5; then
f1.(x,y10) =0.G by A42,A212,A308; then
Q.(f1.(x,y10)) = 0.F by LOPBAN_7:3; then
f2.(x,y10) = 0.F by A51,A212,A308; then
f2/.[x,y10] = 0.F by A50,A212,A308,PARTFUN1:def 6; then
A311: Fai.(x,y10) = y10 - 0.F by A58,A212,A308
.= y10 by RLVECT_1:13;
f.(x,y2) = f/.[x,y2] by A2,A21,A212,A305,A307,PARTFUN1:def 6; then
f/.[x,y20+b] - c = 0.G by A303,A305,RLVECT_1:5; then
f1.(x,y20) =0.G by A42,A212,A309; then
Q.(f1.(x,y20)) = 0.F by LOPBAN_7:3; then
f2.(x,y20) = 0.F by A51,A212,A309; then
f2/.[x,y20] = 0.F by A50,A212,A309,PARTFUN1:def 6; then
Fai.(x,y20) = y20 - 0.F by A58,A212,A309
.= y20 by RLVECT_1:13;
hence y1 = y2
by A213,A240,A249,A253,A302,A304,A305,A311,FIXPOINT2;
end;
A313: a in Ball(a,r0) & b in cl_Ball(b,r2) by A206,A207,LMBALL2;
A314: Eta.a in rng Eta by A206,A282,FUNCT_1:3,LMBALL2;
f.(a,Eta.a) = c by A206,A290,LMBALL2; then
A315: Eta.a = b by A7,A281,A301,A313,A314;
for Eta1,Eta2 be PartFunc of E,F
st dom Eta1 = Ball(a,r0)
& rng Eta1 c= cl_Ball(b,r2)
&(for x be Point of E st x in Ball(a,r0) holds f.(x,Eta1.x) = c)
& dom Eta2 = Ball(a,r0)
& rng Eta2 c= cl_Ball(b,r2)
&(for x be Point of E st x in Ball(a,r0) holds f.(x,Eta2.x) = c )
holds Eta1 = Eta2
proof
let Eta1,Eta2 be PartFunc of E,F;
assume that
A316: dom Eta1 = Ball(a,r0)
& rng Eta1 c=cl_Ball(b,r2)
& (for x be Point of E st x in Ball(a,r0)
holds f.(x,Eta1.x) = c) and
A317: dom Eta2 = Ball(a,r0)
& rng Eta2 c=cl_Ball(b,r2)
& (for x be Point of E st x in Ball(a,r0)
holds f.(x,Eta2.x) = c);
for x be object st x in dom Eta1 holds Eta1.x = Eta2.x
proof
let x0 be object;
assume
A318: x0 in dom Eta1; then
reconsider x = x0 as Point of E;
A319: Eta1.x0 in rng Eta1 by A318,FUNCT_1:3;
A320: Eta2.x0 in rng Eta2 by A316,A317,A318,FUNCT_1:3;
f.(x,Eta1.x) = c & f.(x,Eta2.x) = c by A316,A317,A318;
hence thesis by A301,A316,A317,A318,A319,A320;
end;
hence Eta1 = Eta2 by A316,A317,FUNCT_1:2;
end;
hence thesis by A281,A282,A284,A290,A298,A301,A315,NFCONT_1:19;
end;
theorem
for E,G be RealNormSpace,
F be RealBanachSpace,
Z be Subset of [:E,F:],
f be PartFunc of [:E,F:], G,
a be Point of E,
b be Point of F,
c be Point of G,
z be Point of [:E,F:]
st Z is open & dom f = Z
& f is_continuous_on Z
& f is_partial_differentiable_on`2 Z
& f `partial`2|Z is_continuous_on Z
& z = [a,b] & z in Z
& f.(a,b) = c
& partdiff`2(f,z) is one-to-one
& partdiff`2(f,z)" is Lipschitzian LinearOperator of G,F
holds
ex r1,r2 be Real
st 0 < r1 & 0 < r2
& [:Ball(a,r1),cl_Ball(b,r2):] c= Z
& ( for x be Point of E st x in Ball(a,r1) holds
ex y be Point of F
st y in Ball(b,r2) & f.(x,y) = c )
& ( for x be Point of E st x in Ball(a,r1) holds
( for y1,y2 be Point of F
st y1 in Ball(b,r2) & y2 in Ball(b,r2)
& f.(x,y1) = c & f.(x,y2) = c holds y1=y2 ))
& (ex g be PartFunc of E,F
st g is_continuous_on Ball(a,r1)
& dom g = Ball(a,r1)
& rng g c= Ball(b,r2)
& g.a = b
& for x be Point of E st x in Ball(a,r1) holds f.(x,g.x) = c )
& (for g1,g2 be PartFunc of E,F
st dom g1 = Ball(a,r1)
& rng g1 c= Ball(b,r2)
& (for x be Point of E st x in Ball(a,r1)
holds f.(x,g1.x) = c)
& dom g2 = Ball(a,r1)
& rng g2 c= Ball(b,r2)
& (for x be Point of E st x in Ball(a,r1)
holds f.(x,g2.x) = c)
holds g1=g2)
proof
let E,G be RealNormSpace,
F be RealBanachSpace,
Z be Subset of [:E,F:],
f be PartFunc of [:E,F:], G,
a be Point of E,
b be Point of F,
c be Point of G,
z be Point of [:E,F:] such that
A1: Z is open and
A2: dom f = Z and
A3: f is_continuous_on Z and
A4: f is_partial_differentiable_on`2 Z and
A5: f `partial`2|Z is_continuous_on Z and
A6: z = [a,b] & z in Z and
A7: f.(a,b) = c and
A8: partdiff`2(f,z) is one-to-one and
A9: partdiff`2(f,z)" is Lipschitzian LinearOperator of G,F;
consider r1,r2 be Real such that
A10: 0 < r1 & 0 < r2 and
A11: [:Ball(a,r1),cl_Ball(b,r2):] c= Z and
(for x be Point of E st x in Ball(a,r1) holds
ex y be Point of F st y in cl_Ball(b,r2) & f.(x,y) = c) and
A12: for x be Point of E st x in Ball(a,r1) holds
(for y1,y2 be Point of F
st y1 in cl_Ball(b,r2) & y2 in cl_Ball(b,r2)
& f.(x,y1) = c & f.(x,y2) = c holds y1 = y2) and
A13: (ex g be PartFunc of E,F
st g is_continuous_on Ball(a,r1)
& dom g = Ball(a,r1)
& rng g c= cl_Ball(b,r2)
& g.a = b
& for x be Point of E st x in Ball(a,r1)
holds f.(x,g.x) = c )
& (for g1,g2 be PartFunc of E,F
st dom g1 = Ball(a,r1)
& rng g1 c= cl_Ball(b,r2)
& (for x be Point of E st x in Ball(a,r1)
holds f.(x,g1.x) = c)
& dom g2 = Ball(a,r1)
& rng g2 c= cl_Ball(b,r2)
& (for x be Point of E st x in Ball(a,r1)
holds f.(x,g2.x) = c)
holds g1 = g2) by A1,A2,A3,A4,A5,A6,A7,A8,A9,Th1;
consider g be PartFunc of E,F such that
A14: g is_continuous_on Ball(a,r1)
& dom g = Ball(a,r1)
& rng g c= cl_Ball(b,r2)
& g.a = b
& (for x be Point of E st x in Ball(a,r1)
holds f.(x,g.x) = c)
& (for g1,g2 be PartFunc of E,F
st dom g1 = Ball(a,r1)
& rng g1 c= cl_Ball(b,r2)
& (for x be Point of E st x in Ball(a,r1)
holds f.(x,g1.x) = c)
& dom g2 = Ball(a,r1)
& rng g2 c= cl_Ball(b,r2)
& (for x be Point of E st x in Ball(a,r1)
holds f.(x,g2.x) = c)
holds g1 = g2) by A13;
a in Ball(a,r1) by A10,LMBALL2; then
g | Ball(a,r1) is_continuous_in a by A14,NFCONT_1:def 7; then
consider r3 being Real such that
A15: 0 < r3
& for x1 being Point of E st x1 in dom g & ||.(x1 - a).|| < r3 holds
||.((g /. x1) - (g /. a)).|| < r2 by A10,A14,NFCONT_1:7;
reconsider r0 = min(r1,r3) as Real;
A16: 0 < r0 by A10,A15,XXREAL_0:21;
A17: r0 <= r1 & r0 <=r3 by XXREAL_0:17;
take r0,r2;
thus 0 < r0 & 0 < r2 by A10,A15,XXREAL_0:21;
A18: Ball(a,r0) c= Ball(a,r1)
& Ball(a,r0) c= Ball(a,r3) by A17,LMBALL1; then
A19: [:Ball(a,r0),cl_Ball(b,r2):]
c= [:Ball(a,r1),cl_Ball(b,r2):] by ZFMISC_1:96;
A20: for x be Point of E st x in Ball(a,r0) holds
ex y be Point of F st y in Ball(b,r2) & f.(x,y) = c
proof
let x be Point of E;
assume
A21: x in Ball(a,r0);
A22: g/.x = g.x by A14,A18,A21,PARTFUN1:def 6;
take y = g/.x;
x in Ball(a,r3) by A18,A21; then
ex q be Element of E
st x = q & ||.a - q.|| < r3; then
||.x - a.|| < r3 by NORMSP_1:7; then
||.((g /. x) - (g /. a)).|| < r2 by A14,A15,A18,A21; then
A23: ||.((g /. a) - (g /. x)).|| < r2 by NORMSP_1:7;
g/.a = b by A10,A14,LMBALL2,PARTFUN1:def 6;
hence y in Ball(b,r2) by A23;
thus f.(x,y) = c by A14,A18,A21,A22;
end;
A24: for x be Point of E st x in Ball(a,r0) holds
(for y1,y2 be Point of F
st y1 in Ball(b,r2) & y2 in Ball(b,r2)
& f.(x,y1) = c & f.(x,y2) = c
holds y1 = y2)
proof
let x be Point of E;
assume
A25: x in Ball(a,r0);
let y1,y2 be Point of F;
assume
A26: y1 in Ball(b,r2) & y2 in Ball(b,r2)
& f.(x,y1) = c & f.(x,y2) = c;
Ball(b,r2) c= cl_Ball(b,r2) by LMBALL1;
hence thesis by A12,A18,A25,A26;
end;
reconsider g1= g | Ball(a,r0) as PartFunc of E,F;
g is_continuous_on Ball(a,r0) by A14,A18,NFCONT_1:23; then
A27: g1 is_continuous_on Ball(a,r0) by NFCONT_1:21;
A28: dom g1 = Ball(a,r0) by A14,A17,LMBALL1,RELAT_1:62;
A29: for y be object st y in rng g1 holds y in Ball(b,r2)
proof
let y be object;
assume y in rng g1; then
consider x be object such that
A30: x in dom g1 & y = g1.x by FUNCT_1:def 3;
reconsider x as Point of E by A30;
A31: g/.x = g.x by A14,A18,A28,A30,PARTFUN1:def 6;
A32: g1.x = g.x by A30,FUNCT_1:47;
x in Ball(a,r3) by A18,A28,A30; then
ex q be Element of E
st x = q & ||.a - q.|| < r3; then
||.x - a.|| < r3 by NORMSP_1:7; then
||.((g /. x) - (g /. a)).|| < r2 by A14,A15,A18,A28,A30; then
A33: ||.((g /. a) - (g /. x)).|| < r2 by NORMSP_1:7;
g/.a = b by A10,A14,LMBALL2,PARTFUN1:def 6;
hence y in Ball(b,r2) by A30,A31,A32,A33;
end;
A34: g1.a = b by A14,A16,A28,FUNCT_1:47,LMBALL2;
A35: for x be Point of E st x in Ball(a,r0) holds f.(x,g1.x) = c
proof
let x be Point of E;
assume
A36: x in Ball(a,r0);
hence f.(x,g1.x) = f.(x,g.x) by A28,FUNCT_1:47
.= c by A14,A18,A36;
end;
for g1,g2 be PartFunc of E,F
st dom g1 = Ball(a,r0)
& rng g1 c= Ball(b,r2)
& (for x be Point of E st x in Ball(a,r0)
holds f.(x,g1.x) = c)
& dom g2 = Ball(a,r0)
& rng g2 c= Ball(b,r2)
& (for x be Point of E st x in Ball(a,r0)
holds f.(x,g2.x) = c)
holds g1 = g2
proof
let g1,g2 be PartFunc of E,F;
assume
A38: dom g1 = Ball(a,r0)
& rng g1 c= Ball(b,r2)
& (for x be Point of E st x in Ball(a,r0)
holds f.(x,g1.x) = c)
& dom g2 = Ball(a,r0)
& rng g2 c= Ball(b,r2)
& (for x be Point of E st x in Ball(a,r0)
holds f.(x,g2.x) = c);
for x be object st x in dom g1 holds g1.x = g2.x
proof
let x0 be object;
assume
A39: x0 in dom g1; then
reconsider x = x0 as Point of E;
A40: g1.x0 in rng g1 by A39,FUNCT_1:3; then
reconsider y1 = g1.x0 as Point of F;
A41: g2.x0 in rng g2 by A38,A39,FUNCT_1:3; then
reconsider y2 = g2.x0 as Point of F;
y1 in Ball(b,r2) & y2 in Ball(b,r2)
& f.(x,y1) = c & f.(x,y2) = c by A38,A39,A40,A41;
hence thesis by A24,A38,A39;
end;
hence g1 = g2 by A38,FUNCT_1:2;
end;
hence thesis by A11,A19,A20,A24,A27,A28,A29,
A34,A35,TARSKI:def 3,XBOOLE_1:1;
end;