:: Implicit Function Theorem -- Part {I}
:: by Kazuhisa Nakasho , Yuichi Futa and Yasunari Shidama
::
:: Received November 29, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users

theorem LMNR0: :: NDIFF_8:1

for X, Y being RealNormSpace
for x being Point of X
for y being Point of Y
for z being Point of [:X,Y:] st z = [x,y] holds
||.z.|| = sqrt ((||.x.|| ^2) + (||.y.|| ^2))

proof end;

theorem LMNR1: :: NDIFF_8:2

for X, Y being RealNormSpace
for x being Point of X
for z being Point of [:X,Y:] st z = [x,(0. Y)] holds
||.z.|| = ||.x.||

proof end;

theorem :: NDIFF_8:3

for X, Y being RealNormSpace
for y being Point of Y
for z being Point of [:X,Y:] st z = [(0. X),y] holds
||.z.|| = ||.y.||

proof end;

theorem :: NDIFF_8:4

for X, Y, Z, W being RealNormSpace
for f being Lipschitzian LinearOperator of Z,W
for g being Lipschitzian LinearOperator of Y,Z
for h being Lipschitzian LinearOperator of X,Y holds f * (g * h) = (f * g) * h by RELAT_1:36;

theorem LPB2Th4: :: NDIFF_8:5

for X, Y, Z being RealNormSpace
for g being Lipschitzian LinearOperator of X,Y
for f being Lipschitzian LinearOperator of Y,Z
for h being Lipschitzian LinearOperator of X,Z holds
( h = f * g iff for x being VECTOR of X holds h . x = f . (g . x) )

proof end;

theorem LPB2Th6: :: NDIFF_8:6

for X, Y being RealNormSpace
for f being Lipschitzian LinearOperator of X,Y holds
( f * (id the carrier of X) = f & (id the carrier of Y) * f = f )

proof end;

theorem :: NDIFF_8:7

for X, Y, Z, W being RealNormSpace
for f being Element of BoundedLinearOperators (Z,W)
for g being Element of BoundedLinearOperators (Y,Z)
for h being Element of BoundedLinearOperators (X,Y) holds f * (g * h) = (f * g) * h

proof end;

theorem :: NDIFF_8:8

for X, Y being RealNormSpace
for f being Element of BoundedLinearOperators (X,Y) holds
( f * (FuncUnit X) = f & (FuncUnit Y) * f = f )

proof end;

theorem LPB2Th9: :: NDIFF_8:9

for X, Y, Z being RealNormSpace
for f being Element of (R_NormSpace_of_BoundedLinearOperators (Y,Z))
for g, h being Element of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds f * (g + h) = (f * g) + (f * h)

proof end;

theorem :: NDIFF_8:10

for X, Y, Z being RealNormSpace
for f being Element of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for g, h being Element of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds (g + h) * f = (g * f) + (h * f)

proof end;

theorem LPB2Th11: :: NDIFF_8:11

for X, Y, Z being RealNormSpace
for f being Element of (R_NormSpace_of_BoundedLinearOperators (Y,Z))
for g being Element of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for a, b being Real holds (a * b) * (f * g) = (a * f) * (b * g)

proof end;

theorem :: NDIFF_8:12

for X, Y, Z being RealNormSpace
for f being Element of (R_NormSpace_of_BoundedLinearOperators (Y,Z))
for g being Element of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for a being Real holds a * (f * g) = (a * f) * g

proof end;

definition

let M be RealNormSpace;
let p be Element of M;
let r be Real;

func cl_Ball (p,r) -> Subset of M equals :: NDIFF_8:def 1
{ q where q is Element of M : ||.(p - q).|| <= r } ;

correctness
coherence
{ q where q is Element of M : ||.(p - q).|| <= r } is Subset of M;

proof end;

end;

:: deftheorem defines cl_Ball NDIFF_8:def 1 :
for M being RealNormSpace
for p being Element of M
for r being Real holds cl_Ball (p,r) = { q where q is Element of M : ||.(p - q).|| <= r } ;

theorem LMBALL2: :: NDIFF_8:13

for S being RealNormSpace
for p being Element of S
for r being Real st 0 < r holds
( p in Ball (p,r) & p in cl_Ball (p,r) )

proof end;

theorem :: NDIFF_8:14

for S being RealNormSpace
for p being Element of S
for r being Real st 0 < r holds
( Ball (p,r) <> {} & cl_Ball (p,r) <> {} ) by LMBALL2;

theorem LMBALL1: :: NDIFF_8:15

for M being RealNormSpace
for p being Element of M
for r1, r2 being 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 end;

theorem LMBALL1X: :: NDIFF_8:16

for M being RealNormSpace
for p being Element of M
for r1, r2 being Real st r1 < r2 holds
cl_Ball (p,r1) c= Ball (p,r2)

proof end;

theorem LMBALL: :: NDIFF_8:17

for S being RealNormSpace
for p being Element of S
for r being Real holds Ball (p,r) = { y where y is Point of S : ||.(y - p).|| < r }

proof end;

theorem :: NDIFF_8:18

for S being RealNormSpace
for p being Element of S
for r being Real holds cl_Ball (p,r) = { y where y is Point of S : ||.(y - p).|| <= r }

proof end;

theorem :: NDIFF_8:19

for S being RealNormSpace
for p being Element of S
for r being Real st 0 < r holds
Ball (p,r) is Neighbourhood of p

proof end;

registration

let X be RealNormSpace;
let x be Point of X;
let r be Real;

cluster Ball (x,r) -> open ;

coherence
Ball (x,r) is open

proof end;

cluster cl_Ball (x,r) -> closed ;

coherence
cl_Ball (x,r) is closed

proof end;

end;

theorem NORMSP27: :: NDIFF_8:20

for X being RealNormSpace
for V being Subset of X holds
( V is open iff for x being Point of X st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) )

proof end;

theorem NORMSP35: :: NDIFF_8:21

for X, Y being RealNormSpace
for x being Point of X
for y being Point of Y
for z being Point of [:X,Y:] st z = [x,y] holds
( ||.x.|| <= ||.z.|| & ||.y.|| <= ||.z.|| )

proof end;

theorem NORMSP31: :: NDIFF_8:22

for X, Y being RealNormSpace
for x being Point of X
for y being Point of Y
for z being Point of [:X,Y:]
for r1 being Real st 0 < r1 & z = [x,y] holds
ex r2 being Real st
( 0 < r2 & r2 < r1 & [:(Ball (x,r2)),(Ball (y,r2)):] c= Ball (z,r1) )

proof end;

theorem :: NDIFF_8:23

for X, Y being RealNormSpace
for x being Point of X
for y being Point of Y
for V being Subset of [:X,Y:] st V is open & [x,y] in V holds
ex r being Real st
( 0 < r & [:(Ball (x,r)),(Ball (y,r)):] c= V )

proof end;

theorem :: NDIFF_8:24

for X, Y being RealNormSpace
for x being Point of X
for y being Point of Y
for V being Subset of [:X,Y:]
for r being Real st V = [:(Ball (x,r)),(Ball (y,r)):] holds
V is open

proof end;

theorem LQ2: :: NDIFF_8:25

for E, F being RealNormSpace
for Q being LinearOperator of E,F
for v being Point of E st Q is one-to-one holds
( Q . v = 0. F iff v = 0. E )

proof end;

theorem OP1: :: NDIFF_8:26

for E being RealNormSpace
for X, Y being Subset of E
for v being Point of E st X is open & Y = { (x + v) where x is Point of E : x in X } holds
Y is open

proof end;

theorem OP2: :: NDIFF_8:27

for E being RealNormSpace
for X, Y being Subset of E
for v being Point of E st X is open & Y = { (x - v) where x is Point of E : x in X } holds
Y is open

proof end;

theorem FIXPOINT: :: NDIFF_8:28

for X being RealBanachSpace
for S being non empty Subset of X
for f being PartFunc of X,X st S is closed & dom f = S & rng f c= S & ex k being Real st
( 0 < k & k < 1 & ( for x, y being Point of X st x in S & y in S holds
||.((f /. x) - (f /. y)).|| <= k * ||.(x - y).|| ) ) holds
( ex x0 being Point of X st
( x0 in S & f . x0 = x0 ) & ( for x0, y0 being Point of X st x0 in S & y0 in S & f . x0 = x0 & f . y0 = y0 holds
x0 = y0 ) )

proof end;

theorem FIXPOINT2: :: NDIFF_8:29

for E being RealNormSpace
for F being RealBanachSpace
for E0 being non empty Subset of E
for F0 being non empty Subset of F
for Fai being PartFunc of [:E,F:],F st F0 is closed & [:E0,F0:] c= dom Fai & ( for x being Point of E
for y being Point of F st x in E0 & y in F0 holds
Fai . (x,y) in F0 ) & ( for y being Point of F st y in F0 holds
for x0 being Point of E st x0 in E0 holds
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of E st x1 in E0 & ||.(x1 - x0).|| < d holds
||.((Fai /. [x1,y]) - (Fai /. [x0,y])).|| < e ) ) ) & ex k being Real st
( 0 < k & k < 1 & ( for x being Point of E st x in E0 holds
for y1, y2 being Point of F st y1 in F0 & y2 in F0 holds
||.((Fai /. [x,y1]) - (Fai /. [x,y2])).|| <= k * ||.(y1 - y2).|| ) ) holds
( ( for x being Point of E st x in E0 holds
( ex y being Point of F st
( y in F0 & Fai . (x,y) = y ) & ( for y1, y2 being Point of F st y1 in F0 & y2 in F0 & Fai . (x,y1) = y1 & Fai . (x,y2) = y2 holds
y1 = y2 ) ) ) & ( for x0 being Point of E
for y0 being Point of F st x0 in E0 & y0 in F0 & Fai . (x0,y0) = y0 holds
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of E
for y1 being Point of F st x1 in E0 & y1 in F0 & Fai . (x1,y1) = y1 & ||.(x1 - x0).|| < d holds
||.(y1 - y0).|| < e ) ) ) )

proof end;

theorem FIXPOINT3: :: NDIFF_8:30

for E being RealNormSpace
for F being RealBanachSpace
for A being non empty Subset of E
for B being non empty Subset of F
for Fai being PartFunc of [:E,F:],F st B is closed & [:A,B:] c= dom Fai & ( for x being Point of E
for y being Point of F st x in A & y in B holds
Fai . (x,y) in B ) & ( for y being Point of F st y in B holds
for x0 being Point of E st x0 in A holds
for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of E st x1 in A & ||.(x1 - x0).|| < d holds
||.((Fai /. [x1,y]) - (Fai /. [x0,y])).|| < e ) ) ) & ex k being Real st
( 0 < k & k < 1 & ( for x being Point of E st x in A holds
for y1, y2 being Point of F st y1 in B & y2 in B holds
||.((Fai /. [x,y1]) - (Fai /. [x,y2])).|| <= k * ||.(y1 - y2).|| ) ) holds
( ex g being PartFunc of E,F st
( g is_continuous_on A & dom g = A & rng g c= B & ( for x being Point of E st x in A holds
Fai . (x,(g . x)) = g . x ) ) & ( for g1, g2 being PartFunc of E,F st dom g1 = A & rng g1 c= B & dom g2 = A & rng g2 c= B & ( for x being Point of E st x in A holds
Fai . (x,(g1 . x)) = g1 . x ) & ( for x being Point of E st x in A holds
Fai . (x,(g2 . x)) = g2 . x ) holds
g1 = g2 ) )

proof end;

theorem :: NDIFF_8:31

for E, F being RealNormSpace
for s1, s2 being Point of [:E,F:] st s1 `2 = s2 `2 holds
reproj1 s1 = reproj1 s2

proof end;

theorem REP2: :: NDIFF_8:32

for E, F being RealNormSpace
for s1, s2 being Point of [:E,F:] st s1 `1 = s2 `1 holds
reproj2 s1 = reproj2 s2

proof end;

theorem LMCLOSE2: :: NDIFF_8:33

for E being RealNormSpace
for r being Real
for z, y1, y2 being 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 end;

theorem NEIB1: :: NDIFF_8:34

for E being RealNormSpace
for x, b being Point of E
for N being 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 end;

theorem Th1: :: NDIFF_8:35

for E, G being RealNormSpace
for F being RealBanachSpace
for Z being Subset of [:E,F:]
for f being PartFunc of [:E,F:],G
for a being Point of E
for b being Point of F
for c being Point of G
for z being 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 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (a,r1)),(cl_Ball (b,r2)):] c= Z & ( for x being Point of E st x in Ball (a,r1) holds
ex y being Point of F st
( y in cl_Ball (b,r2) & f . (x,y) = c ) ) & ( for x being Point of E st x in Ball (a,r1) holds
for y1, y2 being 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 being 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 being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) ) & ( for g1, g2 being PartFunc of E,F st dom g1 = Ball (a,r1) & rng g1 c= cl_Ball (b,r2) & ( for x being 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 being Point of E st x in Ball (a,r1) holds
f . (x,(g2 . x)) = c ) holds
g1 = g2 ) )

proof end;

theorem :: NDIFF_8:36

for E, G being RealNormSpace
for F being RealBanachSpace
for Z being Subset of [:E,F:]
for f being PartFunc of [:E,F:],G
for a being Point of E
for b being Point of F
for c being Point of G
for z being 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 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (a,r1)),(cl_Ball (b,r2)):] c= Z & ( for x being Point of E st x in Ball (a,r1) holds
ex y being Point of F st
( y in Ball (b,r2) & f . (x,y) = c ) ) & ( for x being Point of E st x in Ball (a,r1) holds
for y1, y2 being 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 being 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 being Point of E st x in Ball (a,r1) holds
f . (x,(g . x)) = c ) ) & ( for g1, g2 being PartFunc of E,F st dom g1 = Ball (a,r1) & rng g1 c= Ball (b,r2) & ( for x being 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 being Point of E st x in Ball (a,r1) holds
f . (x,(g2 . x)) = c ) holds
g1 = g2 ) )

proof end;