:: Inverse Function Theorem -- Part {I}
:: by Kazuhisa Nakasho and Yuichi Futa
::
:: Received March 30, 2021
:: Copyright (c) 2021 Association of Mizar Users


theorem Th1: :: NDIFF10:1
for X, Y being RealNormSpace
for f being PartFunc of X,Y
for A being Subset of X
for B being Subset of Y st dom f = A & f is_continuous_on A & A is open & B is open holds
f " B is open
proof end;

theorem Th2: :: NDIFF10:2
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, r2 being Real st 0 < r1 & 0 < r2 & z = [x,y] holds
ex s being Real st
( s = min (r1,r2) & s > 0 & Ball (z,s) c= [:(Ball (x,r1)),(Ball (y,r2)):] )
proof end;

theorem Th3: :: NDIFF10:3
for X, Y being RealNormSpace
for V being Subset of [:X,Y:] holds
( V is open iff for x being Point of X
for y being Point of Y st [x,y] in V holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) )
proof end;

theorem Th4: :: NDIFF10:4
for X, Y being RealNormSpace
for V being Subset of [:X,Y:]
for D being Subset of X st D is open & V = [:D, the carrier of Y:] holds
V is open
proof end;

theorem :: NDIFF10:5
for X, Y being RealNormSpace
for V being Subset of [:X,Y:]
for D being Subset of Y st D is open & V = [: the carrier of X,D:] holds
V is open
proof end;

theorem Th6: :: NDIFF10:6
for x, y being Real
for u, v being Element of REAL 2 st u = <*x,y*> & v = <*y,x*> holds
|.u.| = |.v.|
proof end;

definition
let X, Y be RealNormSpace;
func Exch (X,Y) -> LinearOperator of [:X,Y:],[:Y,X:] means :Def1: :: NDIFF10:def 1
( it is one-to-one & it is onto & it is isometric & ( for x being Point of X
for y being Point of Y holds it . (x,y) = [y,x] ) );
existence
ex b1 being LinearOperator of [:X,Y:],[:Y,X:] st
( b1 is one-to-one & b1 is onto & b1 is isometric & ( for x being Point of X
for y being Point of Y holds b1 . (x,y) = [y,x] ) )
proof end;
uniqueness
for b1, b2 being LinearOperator of [:X,Y:],[:Y,X:] st b1 is one-to-one & b1 is onto & b1 is isometric & ( for x being Point of X
for y being Point of Y holds b1 . (x,y) = [y,x] ) & b2 is one-to-one & b2 is onto & b2 is isometric & ( for x being Point of X
for y being Point of Y holds b2 . (x,y) = [y,x] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Exch NDIFF10:def 1 :
for X, Y being RealNormSpace
for b3 being LinearOperator of [:X,Y:],[:Y,X:] holds
( b3 = Exch (X,Y) iff ( b3 is one-to-one & b3 is onto & b3 is isometric & ( for x being Point of X
for y being Point of Y holds b3 . (x,y) = [y,x] ) ) );

theorem Th7: :: NDIFF10:7
for X, Y being RealNormSpace
for Z being Subset of [:X,Y:]
for x, y being object holds
( [x,y] in Z iff [y,x] in (Exch (Y,X)) " Z )
proof end;

theorem Th8: :: NDIFF10:8
for X, Y being RealNormSpace
for Z being non empty set
for f being PartFunc of [:X,Y:],Z
for I being Function of [:Y,X:],[:X,Y:] st ( for y being Point of Y
for x being Point of X holds I . (y,x) = [x,y] ) holds
( dom (f * I) = I " (dom f) & ( for x being Point of X
for y being Point of Y holds (f * I) . (y,x) = f . (x,y) ) )
proof end;

theorem Th9: :: NDIFF10:9
for X, Y, Z being RealNormSpace
for f being PartFunc of Y,Z
for I being LinearOperator of X,Y
for V being Subset of Y st f is_differentiable_on V & I is one-to-one & I is onto & I is isometric holds
for y being Point of Y st y in V holds
(f `| V) . y = (((f * I) `| (I " V)) /. ((I ") . y)) * (I ")
proof end;

theorem Th10: :: NDIFF10:10
for X, Y, Z being RealNormSpace
for V being Subset of Y
for g being PartFunc of Y,Z
for I being LinearOperator of X,Y st I is one-to-one & I is onto & I is isometric & g is_differentiable_on V holds
( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V )
proof end;

theorem Th11: :: NDIFF10:11
for X, Y, Z being RealNormSpace
for f being PartFunc of [:X,Y:],Z
for U being Subset of [:X,Y:]
for I being Function of [:Y,X:],[:X,Y:] st ( for y being Point of Y
for x being Point of X holds I . (y,x) = [x,y] ) holds
for a being Point of X
for b being Point of Y
for u being Point of [:X,Y:]
for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds
( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )
proof end;

theorem :: NDIFF10:12
for X, Y, Z being RealNormSpace
for f being PartFunc of [:X,Y:],Z
for U being Subset of [:X,Y:]
for I being LinearOperator of [:Y,X:],[:X,Y:] st U = dom f & f is_differentiable_on U & I is one-to-one & I is onto & I is isometric & ( for y being Point of Y
for x being Point of X holds I . (y,x) = [x,y] ) holds
for a being Point of X
for b being Point of Y
for u being Point of [:X,Y:]
for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds
( ( f is_partial_differentiable_in`1 u implies f * I is_partial_differentiable_in`2 v ) & ( f * I is_partial_differentiable_in`2 v implies f is_partial_differentiable_in`1 u ) & ( f is_partial_differentiable_in`2 u implies f * I is_partial_differentiable_in`1 v ) & ( f * I is_partial_differentiable_in`1 v implies f is_partial_differentiable_in`2 u ) ) by Th11;

theorem :: NDIFF10:13
for X, Y, Z being RealNormSpace
for f being PartFunc of [:X,Y:],Z
for U being Subset of [:X,Y:]
for I being LinearOperator of [:Y,X:],[:X,Y:] st U = dom f & f is_differentiable_on U & I is one-to-one & I is onto & I is isometric & ( for y being Point of Y
for x being Point of X holds I . (y,x) = [x,y] ) holds
for a being Point of X
for b being Point of Y
for u being Point of [:X,Y:]
for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds
( partdiff`1 (f,u) = partdiff`2 ((f * I),v) & partdiff`2 (f,u) = partdiff`1 ((f * I),v) ) by Th11;

theorem Th14: :: NDIFF10:14
for F being RealNormSpace
for G, E being non trivial 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_differentiable_on Z & f `| Z is_continuous_on Z & [a,b] in Z & f . (a,b) = c & z = [a,b] & partdiff`1 (f,z) is invertible holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(cl_Ball (a,r1)),(Ball (b,r2)):] c= Z & ( for y being Point of F st y in Ball (b,r2) holds
ex x being Point of E st
( x in Ball (a,r1) & f . (x,y) = c ) ) & ( for y being Point of F st y in Ball (b,r2) holds
for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f . (x1,y) = c & f . (x2,y) = c holds
x1 = x2 ) & ex g being PartFunc of F,E st
( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds
f . ((g . y),y) = c ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F
for z being Point of [:E,F:] st y in Ball (b,r2) & z = [(g . y),y] holds
diff (g,y) = - ((Inv (partdiff`1 (f,z))) * (partdiff`2 (f,z))) ) & ( for y being Point of F
for z being Point of [:E,F:] st y in Ball (b,r2) & z = [(g . y),y] holds
partdiff`1 (f,z) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds
f . ((g1 . y),y) = c ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds
f . ((g2 . y),y) = c ) holds
g1 = g2 ) )
proof end;

theorem Th15: :: NDIFF10:15
for E, F being non trivial RealBanachSpace
for D being Subset of E
for f being PartFunc of E,F
for f1 being PartFunc of [:E,F:],F
for Z being Subset of [:E,F:] st D is open & dom f = D & D <> {} & f is_differentiable_on D & f `| D is_continuous_on D & Z = [:D, the carrier of F:] & dom f1 = Z & ( for s being Point of E
for t being Point of F st s in D holds
f1 . (s,t) = (f /. s) - t ) holds
( f1 is_differentiable_on Z & f1 `| Z is_continuous_on Z & ( for x being Point of E
for y being Point of F
for z being Point of [:E,F:] st x in D & z = [x,y] holds
ex I being Point of (R_NormSpace_of_BoundedLinearOperators (F,F)) st
( I = id the carrier of F & partdiff`1 (f1,z) = diff (f,x) & partdiff`2 (f1,z) = - I ) ) )
proof end;

theorem Th16: :: NDIFF10:16
for E, F being non trivial RealBanachSpace
for Z being Subset of E
for f being PartFunc of E,F
for a being Point of E
for b being Point of F st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & a in Z & f . a = b & diff (f,a) is invertible holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & cl_Ball (a,r1) c= Z & ( for y being Point of F st y in Ball (b,r2) holds
ex x being Point of E st
( x in Ball (a,r1) & f /. x = y ) ) & ( for y being Point of F st y in Ball (b,r2) holds
for x1, x2 being Point of E st x1 in Ball (a,r1) & x2 in Ball (a,r1) & f /. x1 = y & f /. x2 = y holds
x1 = x2 ) & ex g being PartFunc of F,E st
( dom g = Ball (b,r2) & rng g c= Ball (a,r1) & g is_continuous_on Ball (b,r2) & g . b = a & ( for y being Point of F st y in Ball (b,r2) holds
f /. (g /. y) = y ) & g is_differentiable_on Ball (b,r2) & g `| (Ball (b,r2)) is_continuous_on Ball (b,r2) & ( for y being Point of F st y in Ball (b,r2) holds
diff (g,y) = Inv (diff (f,(g /. y))) ) & ( for y being Point of F st y in Ball (b,r2) holds
diff (f,(g /. y)) is invertible ) ) & ( for g1, g2 being PartFunc of F,E st dom g1 = Ball (b,r2) & rng g1 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds
f /. (g1 . y) = y ) & dom g2 = Ball (b,r2) & rng g2 c= Ball (a,r1) & ( for y being Point of F st y in Ball (b,r2) holds
f /. (g2 . y) = y ) holds
g1 = g2 ) )
proof end;

theorem Th17: :: NDIFF10:17
for E, F being non trivial RealBanachSpace
for Z being Subset of E
for f being PartFunc of E,F
for a being Point of E
for b being Point of F st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & a in Z & f . a = b & diff (f,a) is invertible holds
ex A being Subset of E ex B being Subset of F ex g being PartFunc of F,E st
( A is open & B is open & A c= dom f & a in A & b in B & f .: A = B & dom g = B & rng g = A & dom (f | A) = A & rng (f | A) = B & f | A is one-to-one & g is one-to-one & g = (f | A) " & f | A = g " & g . b = a & g is_continuous_on B & g is_differentiable_on B & g `| B is_continuous_on B & ( for y being Point of F st y in B holds
diff (f,(g /. y)) is invertible ) & ( for y being Point of F st y in B holds
diff (g,y) = Inv (diff (f,(g /. y))) ) )
proof end;

theorem Th18: :: NDIFF10:18
for E, F being non trivial RealBanachSpace
for Z being Subset of E
for f being PartFunc of E,F
for a being Point of E
for b being Point of F st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & a in Z & f . a = b & diff (f,a) is invertible holds
for r1 being Real st 0 < r1 holds
ex r2 being Real st
( 0 < r2 & Ball (b,r2) c= f .: (Ball (a,r1)) )
proof end;

theorem :: NDIFF10:19
for E, F being non trivial RealBanachSpace
for Z being Subset of E
for f being PartFunc of E,F st Z is open & dom f = Z & f is_differentiable_on Z & f `| Z is_continuous_on Z & ( for x being Point of E st x in Z holds
diff (f,x) is invertible ) holds
( ( for x being Point of E
for r1 being Real st x in Z & 0 < r1 holds
ex y being Point of F ex r2 being Real st
( y = f . x & 0 < r2 & Ball (y,r2) c= f .: (Ball (x,r1)) ) ) & f .: Z is open )
proof end;