:: Inverse Function Theorem -- Part {I}
::  by Kazuhisa Nakasho and Yuichi Futa
:: 
:: Received March 30, 2021
:: Copyright (c) 2021 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, RELAT_1, LOPBAN_1, RCOMP_1, SQUARE_1, TARSKI,
      ARYTM_3, ALGSTR_0, PRALG_1, FUNCT_2, ARYTM_1, SUPINF_2, FCONT_1,
      STRUCT_0, CARD_1, XXREAL_0, XBOOLE_0, FINSEQ_1, RLVECT_1, CFCONT_1,
      NDIFF_7, MCART_1, METRIC_1, LOPBAN_2, FUNCOP_1, NDIFF10, VECTMETR,
      MSSUBFAM, COMPLEX1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
      RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, BINOP_1, NUMBERS, XCMPLX_0,
      XXREAL_0, XREAL_0, SQUARE_1, NAT_1, FINSEQ_1, FINSEQ_2, STRUCT_0,
      PRE_TOPC, RLVECT_1, VECTSP_1, NORMSP_0, NORMSP_1, VFUNCT_1, EUCLID,
      LOPBAN_1, LOPBAN_2, LOPBAN_5, LOPBAN_7, NFCONT_1, NDIFF_1, MAZURULM,
      NDIFF_2, PRVECT_3, NDIFF_7, NDIFF_8, LOPBAN13;
 constructors SQUARE_1, VFUNCT_1, NDIFF_1, RELSET_1, RSSPACE3, LOPBAN_3,
      NDIFF_2, DOMAIN_1, NDIFF_7, NDIFF_8, LOPBAN_5, LOPBAN_7, LOPBAN13,
      RVSUM_1;
 registrations RELSET_1, STRUCT_0, XREAL_0, MEMBERED, FUNCT_1, FUNCT_2,
      LOPBAN_1, LOPBAN_2, PRVECT_3, VALUED_0, XTUPLE_0, NDIFF_7, RELAT_1,
      NDIFF_8, SQUARE_1, NORMSP_3;
 requirements SUBSET, REAL, BOOLE, NUMERALS;


begin :: Preliminaries

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 :: NDIFF10:1
  for X,Y be RealNormSpace,
      f be PartFunc of X,Y,
      A be Subset of X,
      B be Subset of Y
  st dom f = A
   & f is_continuous_on A
   & A is open
   & B is open
  holds f"B is open;

theorem :: NDIFF10:2
  for X,Y be RealNormSpace,
        x be Point of X,
        y be Point of Y,
        z be Point of [:X,Y:],
    r1,r2 be Real st 0 < r1 & 0 < r2 & z = [x,y]
  holds
    ex s be Real
    st s = min(r1, r2) & s > 0
     & Ball(z,s) c= [:Ball(x,r1), Ball(y,r2):];

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

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

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

begin :: A map to reverse the order of product of two norm spaces

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

definition
  let X,Y be RealNormSpace;
  func Exch(X,Y) -> LinearOperator of [:X,Y:],[:Y,X:]
  means
:: NDIFF10:def 1

    it is one-to-one onto isometric
  & for x be Point of X,y be Point of Y
    holds it.(x,y) = [y,x];
end;

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

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

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

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

theorem :: NDIFF10:11
  for X,Y,Z be RealNormSpace,
          f be PartFunc of [:X,Y:],Z,
          U be Subset of [:X,Y:],
          I be Function of [:Y,X:],[:X,Y:]
   st ( for y be Point of Y,x be Point of X
        holds I.(y,x) = [x,y] )
  holds
    for a be Point of X, b be Point of Y,
        u be Point of [:X,Y:],
        v be 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);

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

theorem :: NDIFF10:13
  for X,Y,Z be RealNormSpace,
          f be PartFunc of [:X,Y:],Z,
          U be Subset of [:X,Y:],
          I be LinearOperator of [:Y,X:],[:X,Y:]
   st U = dom f
    & f is_differentiable_on U
    & I is one-to-one onto isometric
    & ( for y be Point of Y,x be Point of X
        holds I.(y,x) = [x,y] )
  holds
    for a be Point of X, b be Point of Y,
        u be Point of [:X,Y:],
        v be 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);

begin :: Application of implicit function theorem

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

theorem :: NDIFF10:15
  for E,F be non trivial RealBanachSpace,
      D be Subset of E,
      f be PartFunc of E,F,
      f1 be PartFunc of [:E,F:],F,
      Z be 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 be Point of E,
          t be 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 be Point of E,y be Point of F,
        z be Point of [:E,F:]
     st x in D & z = [x,y]
    holds
      ex I be 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;

theorem :: NDIFF10:16
  for E,F be non trivial RealBanachSpace,
      Z be Subset of E,
      f be PartFunc of E,F,
      a be Point of E,
      b be 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 be Real
    st
      0 < r1 & 0 < r2
     & cl_Ball(a,r1) c= Z
     & (for y be Point of F st y in Ball(b,r2) holds
         ex x be Point of E
         st x in Ball(a,r1) & f/.x = y)
     & (for y be Point of F st y in Ball(b,r2) holds
         for x1,x2 be 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 be 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 be 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 be Point of F
              st y in Ball(b,r2)
              holds diff(g,y) = Inv diff(f,g/.y) )
          & ( for y be Point of F
              st y in Ball(b,r2)
              holds diff(f,g/.y) is invertible ) )
     & ( for g1,g2 be PartFunc of F,E
         st dom g1 = Ball(b,r2)
          & rng g1 c= Ball(a,r1)
          & ( for y be 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 be Point of F st y in Ball(b,r2)
              holds f/.(g2.y) = y )
         holds g1 = g2 );

begin :: Inverse function theorem for class C^1 functions

theorem :: NDIFF10:17
  for E,F be non trivial RealBanachSpace,
      Z be Subset of E,
      f be PartFunc of E,F,
      a be Point of E,
      b be 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 be Subset of E,B be Subset of F,
       g be 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 be Point of F st y in B
         holds diff(f,g/.y) is invertible )
     & ( for y be Point of F st y in B
         holds diff(g,y) = Inv diff(f,g/.y) );

theorem :: NDIFF10:18
  for E,F be non trivial RealBanachSpace,
      Z be Subset of E,
      f be PartFunc of E,F,
      a be Point of E,
      b be 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 be Real st 0 < r1
     holds
       ex r2 be Real
       st 0 < r2 & Ball(b,r2) c= f.: Ball(a,r1) );

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