:: 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 :: (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; 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 :: NDIFF_8:1 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); theorem :: NDIFF_8:2 for X,Y be RealNormSpace, x be Point of X, z be Point of [:X,Y:] st z = [x,0.Y] holds ||.z.|| = ||.x.||; theorem :: NDIFF_8:3 for X,Y be RealNormSpace, y be Point of Y, z be Point of [:X,Y:] st z = [0.X,y] holds ||.z.|| = ||.y.||; theorem :: NDIFF_8:4 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; theorem :: NDIFF_8:5 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); theorem :: NDIFF_8:6 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; theorem :: NDIFF_8:7 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; theorem :: NDIFF_8:8 for X,Y be RealNormSpace for f be Element of BoundedLinearOperators (X,Y) holds f * FuncUnit(X) = f & FuncUnit(Y) * f = f; theorem :: NDIFF_8:9 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; theorem :: NDIFF_8:10 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; theorem :: NDIFF_8:11 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); theorem :: NDIFF_8:12 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; 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 :: NDIFF_8:def 1 {q where q is Element of M : ||.p - q.|| <= r}; end; theorem :: NDIFF_8:13 for p be Element of S, r be Real st 0 < r holds p in Ball(p,r) & p in cl_Ball(p,r); theorem :: NDIFF_8:14 for p be Element of S, r be Real st 0 < r holds Ball(p,r) <> {} & cl_Ball(p,r) <> {}; theorem :: NDIFF_8:15 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); theorem :: NDIFF_8:16 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); theorem :: NDIFF_8:17 for p be Element of S, r be Real holds Ball(p,r) = {y where y is Point of S: ||.y - p.|| < r}; theorem :: NDIFF_8:18 for p be Element of S, r be Real holds cl_Ball(p,r) = {y where y is Point of S: ||.y - p.|| <= r}; theorem :: NDIFF_8:19 for p be Element of S, r be Real st 0 < r holds Ball(p,r) is Neighbourhood of p; registration let X be RealNormSpace, x be Point of X, r be Real; cluster Ball(x,r) -> open; cluster cl_Ball(x,r) -> closed; end; theorem :: NDIFF_8:20 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; theorem :: NDIFF_8:21 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.||; theorem :: NDIFF_8:22 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); theorem :: NDIFF_8:23 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; theorem :: NDIFF_8:24 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; theorem :: NDIFF_8:25 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; theorem :: NDIFF_8:26 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; theorem :: NDIFF_8:27 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; begin :: 3. Existence and uniqueness of continuous implicit function theorem :: NDIFF_8:28 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); theorem :: NDIFF_8:29 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))); theorem :: NDIFF_8:30 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); theorem :: NDIFF_8:31 for E,F be RealNormSpace, s1,s2 be Point of [:E,F:] st s1`2 = s2`2 holds reproj1 s1 = reproj1 s2; theorem :: NDIFF_8:32 for E,F be RealNormSpace, s1,s2 be Point of [:E,F:] st s1`1 = s2`1 holds reproj2 s1 = reproj2 s2; theorem :: NDIFF_8:33 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); theorem :: NDIFF_8:34 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; theorem :: NDIFF_8:35 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); theorem :: NDIFF_8:36 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);