:: Inverse Function Theorem -- Part {I}
:: by Kazuhisa Nakasho and Yuichi Futa
::
:: Received March 30, 2021
:: Copyright (c) 2021-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, 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;
definitions TARSKI;
equalities RLVECT_1, LOPBAN_1, NDIFF_2, BINOP_1, PRVECT_3, LOPBAN_2, LOPBAN_5,
XBOOLE_0, NDIFF_7;
expansions RELAT_1, NDIFF_7, MAZURULM, VECTSP_1, XBOOLE_0, FUNCT_2;
theorems TARSKI, XBOOLE_0, XBOOLE_1, RLVECT_1, ZFMISC_1, RELAT_1, FUNCT_1,
VFUNCT_1, FUNCT_2, LOPBAN_1, PARTFUN1, NFCONT_1, NDIFF_1, XXREAL_0,
NORMSP_0, PRVECT_3, NDIFF_7, FUNCOP_1, LOPBAN_7, EUCLID_3, FINSEQ_1,
NDIFF_8, XTUPLE_0, LOPBAN13, NDIFF_9, RELSET_1, BINOP_1;
schemes FUNCT_2, BINOP_1;
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 Th1:
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
proof
let X,Y be RealNormSpace,
f be PartFunc of X,Y,
A be Subset of X,
B be Subset of Y;
assume that
A1: dom f = A and
A2: f is_continuous_on A and
A3: A is open and
A4: B is open;
for a being Point of X st a in f"B holds
ex s being Real st
s > 0 & Ball(a,s) c= f"B
proof
let a be Point of X;
assume a in f"B; then
A6: a in dom f & f.a in B by FUNCT_1:def 7; then
f/.a in B by PARTFUN1:def 6; then
consider t be Real such that
A7: t > 0 & Ball(f/.a, t) c= B by A4,NDIFF_8:20;
consider s0 being Real such that
A8: 0 < s0
& for a1 being Point of X st a1 in A & ||.(a1 - a).|| < s0 holds
||.(f /. a1) - (f /. a).|| < t by A1,A2,A6,A7,NFCONT_1:19;
consider s1 be Real such that
A9: 0 < s1 & Ball(a,s1) c= A by A1,A3,A6,NDIFF_8:20;
set s = min(s0,s1);
A10: s <= s0 by XXREAL_0:17;
A11: s <= s1 by XXREAL_0:17;
take s;
thus 0 < s by A8,A9,XXREAL_0:15;
for a1 be object st a1 in Ball(a,s) holds a1 in f"B
proof
let a1 be object;
assume
A13: a1 in Ball(a,s); then
reconsider a1 as Point of X;
A14: a1 in Ball(a,s1) by A11,A13,NDIFF_8:15,TARSKI:def 3;
A15: a1 in Ball(a,s0) by A10,A13,NDIFF_8:15,TARSKI:def 3;
a1 in { x where x is Point of X : ||.(x - a).|| < s0 }
by A15,NDIFF_8:17; then
ex x be Point of X st a1 = x & ||.(x - a).|| < s0; then
||.(f /. a1) - (f /. a).|| < t by A8,A9,A14; then
f /. a1 in { y where y is Point of Y : ||.(y - f/.a).|| < t }; then
f /. a1 in Ball(f/.a, t) by NDIFF_8:17; then
f . a1 in Ball(f/.a, t) by A1,A9,A14,PARTFUN1:def 6;
hence thesis by A1,A7,A9,A14,FUNCT_1:def 7;
end;
hence Ball(a,s) c= f"B by TARSKI:def 3;
end;
hence f"B is open by NDIFF_8:20;
end;
theorem Th2:
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):]
proof
let X,Y be RealNormSpace,
x be Point of X,
y be Point of Y,
z be Point of [:X,Y:],
r1,r2 be Real;
assume
A1: 0 < r1 & 0 < r2 & z = [x,y];
take s = min(r1,r2);
Ball(z,s) c= [:(Ball (x,r1)),(Ball (y,r2)):]
proof
let z1 be object;
assume
A3: z1 in Ball(z,s); then
reconsider z1 as Point of [:X,Y:];
A4: ex z2 be Point of [:X,Y:] st z2 = z1 & ||.z - z2.|| < s by A3;
consider x1 be Point of X, y1 be Point of Y such that
A5: z1 = [x1, y1] by PRVECT_3:18;
-z1 = [-x1,-y1] by A5,PRVECT_3:18; then
z - z1 = [x - x1, y - y1] by A1,PRVECT_3:18; then
||.x - x1.|| <= ||.z - z1.||
& ||.y - y1.|| <= ||.z - z1.|| by NDIFF_8:21; then
A6: ||.x - x1.|| < s & ||.y - y1.|| < s by A4,XXREAL_0:2;
s <= r1 & s <= r2 by XXREAL_0:17; then
||.x - x1.|| < r1 & ||.y - y1.|| < r2 by A6,XXREAL_0:2; then
x1 in Ball(x,r1) & y1 in Ball(y,r2);
hence thesis by A5,ZFMISC_1:87;
end;
hence thesis by A1,XXREAL_0:15;
end;
theorem Th3:
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)
proof
let X,Y be RealNormSpace,
V be Subset of [:X,Y:];
hereby
assume
A1: V is open;
let x be Point of X, y be Point of Y;
assume [x,y] in V; then
consider r be Real such that
A2: 0 < r & [:Ball(x,r),Ball(y,r):] c= V by A1,NDIFF_8:23;
thus
ex r1,r2 be Real
st 0 < r1 & 0 < r2
& [:Ball(x,r1),Ball(y,r2):] c= V by A2;
end;
assume
A3: 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;
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
A4: z in V;
consider x be Point of X, y be Point of Y such that
A5: z = [x,y] by PRVECT_3:18;
consider r1,r2 be Real such that
A6: 0 < r1 & 0 < r2
& [:Ball(x,r1),Ball(y,r2):] c= V by A3,A4,A5;
consider s be Real such that
A7: s = min(r1, r2) & s > 0 and
A8: Ball(z,s) c= [:Ball(x,r1), Ball(y,r2):] by A5,A6,Th2;
take s;
thus thesis by A6,A7,A8,XBOOLE_1:1;
end;
hence V is open by NDIFF_8:20;
end;
theorem Th4:
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
proof
let X,Y be RealNormSpace,
V be Subset of [:X,Y:],
D be Subset of X;
assume
A1: D is open & V = [:D,the carrier of Y:];
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
proof
let x be Point of X, y be Point of Y;
assume [x,y] in V; then
x in D & y in the carrier of Y by A1,ZFMISC_1:87; then
consider r be Real such that
A2: r > 0 & Ball(x,r) c= D by A1,NDIFF_8:20;
[:Ball(x,r),Ball(y,r):] c= V
proof
let z be object;
assume z in [:Ball(x,r),Ball(y,r):]; then
consider qx,qy be object such that
A4: qx in Ball(x,r) & qy in Ball(y,r)
& z = [qx,qy] by ZFMISC_1:def 2;
thus z in V by A1,A2,A4,ZFMISC_1:87;
end;
hence thesis by A2;
end;
hence thesis by Th3;
end;
theorem
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
proof
let X,Y be RealNormSpace,
V be Subset of [:X,Y:],
D be Subset of Y;
assume
A1: D is open & V = [:the carrier of X,D:];
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
proof
let x be Point of X, y be Point of Y;
assume [x,y] in V; then
x in the carrier of X & y in D by A1,ZFMISC_1:87; then
consider r be Real such that
A2: r > 0 & Ball(y,r) c= D by A1,NDIFF_8:20;
[:Ball(x,r),Ball(y,r):] c= V
proof
let z be object;
assume z in [:Ball(x,r),Ball(y,r):]; then
consider qx,qy be object such that
A4: qx in Ball(x,r) & qy in Ball(y,r)
& z = [qx,qy] by ZFMISC_1:def 2;
thus z in V by A1,A2,A4,ZFMISC_1:87;
end;
hence thesis by A2;
end;
hence thesis by Th3;
end;
begin :: A map to reverse the order of product of two norm spaces
theorem Th6:
for x,y be Real, u,v being Element of REAL 2
st u = <*x,y*> & v = <*y,x*>
holds |.u.| = |.v.|
proof
let x,y be Real, u,v be Element of REAL 2;
assume
A1: u = <*x,y*> & v = <*y,x*>; then
A3: len v = 2 & v.1 = y & v.2 = x by FINSEQ_1:44;
len u = 2 & u.1 = x & u.2 = y by A1,FINSEQ_1:44;
hence |.u.| = sqrt (x^2 + y^2) by EUCLID_3:22
.= |.v.| by A3,EUCLID_3:22;
end;
definition
let X,Y be RealNormSpace;
func Exch(X,Y) -> LinearOperator of [:X,Y:],[:Y,X:]
means
:Def1:
it is one-to-one onto isometric
& for x be Point of X,y be Point of Y
holds it.(x,y) = [y,x];
existence
proof
defpred P1[ object , object , object ]
means
$3 = [$2,$1];
A1: for x being Element of the carrier of X
for y being Element of the carrier of Y
ex z being Element of the carrier of [:Y,X:] st P1[x,y,z]
proof
let x be Element of the carrier of X,
y be Element of the carrier of Y;
[y,x] is Point of [:Y,X:];
hence thesis;
end;
consider f being Function of [:the carrier of X,the carrier of Y:],
the carrier of [:Y,X:] such that
A2: for x being Element of the carrier of X
for y being Element of the carrier of Y
holds P1[x, y, f.(x,y)]
from BINOP_1:sch 3(A1);
reconsider f as Function of [:X,Y:], [:Y,X:];
for p1, p2 being Point of [:X,Y:] holds
f.(p1+p2) = f.p1 + f.p2
proof
let p1, p2 be Point of [:X,Y:];
consider x1 be Point of X, y1 be Point of Y such that
A4: p1 = [x1,y1] by PRVECT_3:18;
consider x2 be Point of X, y2 be Point of Y such that
A5: p2 = [x2,y2] by PRVECT_3:18;
reconsider q1 = [y1,x1] as Point of [:Y,X:];
reconsider q2 = [y2,x2] as Point of [:Y,X:];
A8: f.p1 = f.(x1,y1) by A4
.= q1 by A2;
A9: f.p2 = f.(x2,y2) by A5
.= q2 by A2;
thus f.(p1+p2) = f.(x1+x2,y1+y2) by A4,A5,PRVECT_3:18
.= [y1+y2,x1+x2] by A2
.= f.p1 + f.p2 by A8,A9,PRVECT_3:18;
end; then
A10: f is additive;
for p being Point of [:X,Y:]
for r being Real holds f.(r * p) = r * (f.p)
proof
let p be Point of [:X,Y:],
r be Real;
consider x be Point of X,y be Point of Y such that
A11: p = [x,y] by PRVECT_3:18;
reconsider q = [y,x] as Point of [:Y,X:];
reconsider rq = [r*y,r*x] as Point of [:Y,X:];
A12: f.p = f.(x,y) by A11
.= q by A2;
thus f.(r*p) = f.(r*x,r*y) by A11,PRVECT_3:18
.= [r*y,r*x] by A2
.= r*f.p by A12,PRVECT_3:18;
end; then
reconsider f as LinearOperator of [:X,Y:],[:Y,X:] by A10,LOPBAN_1:def 5;
take f;
A14: for p1,p2 be object
st p1 in the carrier of [:X,Y:]
& p2 in the carrier of [:X,Y:]
& f.p1 = f.p2
holds p1 = p2
proof
let p1,p2 be object;
assume
A15: p1 in the carrier of [:X,Y:]
& p2 in the carrier of [:X,Y:]
& f.p1 = f.p2;
consider x1 be Point of X,y1 be Point of Y such that
A16: p1 = [x1,y1] by A15,PRVECT_3:18;
consider x2 be Point of X,y2 be Point of Y such that
A17: p2 = [x2,y2] by A15,PRVECT_3:18;
A18: f.p1 = f.(x1,y1) by A16
.= [y1,x1] by A2;
f.p2 = f.(x2,y2) by A17
.= [y2,x2] by A2; then
x1 = x2 & y1 = y2 by A15,A18,XTUPLE_0:1;
hence thesis by A16,A17;
end;
for q be object st q in the carrier of [:Y,X:]
holds q in rng f
proof
let q be object;
assume q in the carrier of [:Y,X:]; then
consider y be Point of Y,x be Point of X such that
A22: q = [y,x] by PRVECT_3:18;
reconsider p = [x,y] as Point of [:X,Y:];
f.p = f.(x,y)
.= q by A2,A22;
hence q in rng f by FUNCT_2:4;
end; then
rng f = the carrier of [:Y,X:] by TARSKI:def 3;
hence f is one-to-one onto by A14,FUNCT_2:19;
for p being Point of [:X,Y:] holds ||. f.p .|| = ||.p.||
proof
let p be Point of [:X,Y:];
consider x be Point of X,y be Point of Y such that
A23: p = [x,y] by PRVECT_3:18;
reconsider q = [y,x] as Point of [:Y,X:];
A24: f.p = f.(x,y) by A23
.= q by A2;
consider u being Element of REAL 2 such that
A25: u = <*||.x.||,||.y.||*> & ||.p.|| = |.u.| by A23,PRVECT_3:18;
consider v be Element of REAL 2 such that
A26: v = <*||.y.||,||.x.||*> & ||.q.|| = |.v.| by PRVECT_3:18;
thus ||.f.p.|| = ||.p.|| by A24,A25,A26,Th6;
end;
hence f is isometric by NDIFF_7:7;
thus thesis by A2;
end;
uniqueness
proof
let f, g be LinearOperator of [:X,Y:],[:Y,X:];
assume
A27: f is one-to-one onto isometric
& for x be Point of X,y be Point of Y
holds f.(x,y) = [y,x];
assume
A28: g is one-to-one onto isometric
& for x be Point of X,y be Point of Y
holds g.(x,y) = [y,x];
for x, y being set
st x in the carrier of X
& y in the carrier of Y
holds f.(x,y) = g.(x,y)
proof
let x, y be set;
assume
A29: x in the carrier of X
& y in the carrier of Y; then
reconsider x1 = x as Point of X;
reconsider y1 = y as Point of Y by A29;
thus f.(x,y) = [y1,x1] by A27
.= g.(x,y) by A28;
end;
hence f = g by BINOP_1:def 21;
end;
end;
theorem Th7:
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
proof
let X,Y be RealNormSpace,
Z be Subset of [:X,Y:],
x,y be object;
set I = Exch(Y,X);
hereby
assume
A1: [x,y] in Z; then
consider x1 be Point of X, y1 be Point of Y such that
A2: [x,y] = [x1,y1] by PRVECT_3:18;
A3: x = x1 & y = y1 by A2,XTUPLE_0:1;
A4: [x,y] = I.(y1,x1) by A2,Def1
.= I.[y,x] by A3;
[y1,x1] in the carrier of [:Y,X:];
hence [y,x] in I"Z by A1,A3,A4,FUNCT_2:38;
end;
assume
A5: [y,x] in I"Z; then
consider y1 be Point of Y, x1 be Point of X such that
A6: [y,x] = [y1,x1] by PRVECT_3:18;
A7: x = x1 & y = y1 by A6,XTUPLE_0:1;
I.[y,x] = I.(y1,x1) by A6
.= [x,y] by A7,Def1;
hence [x,y] in Z by A5,FUNCT_2:38;
end;
theorem Th8:
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)
proof
let X,Y be RealNormSpace,
Z be non empty set,
f be PartFunc of [:X,Y:],Z,
I be Function of [:Y,X:],[:X,Y:];
assume
A1: for x be Point of Y,y be Point of X
holds I.(x,y) = [y,x];
for w be object holds
w in dom(f*I) iff w in I"(dom f)
proof
let w be object;
w in dom(f*I) iff w in dom I & I.w in dom f by FUNCT_1:11;
hence w in dom (f*I) iff w in I"(dom f) by FUNCT_1:def 7;
end;
hence dom(f*I) = I"(dom f) by TARSKI:2;
let x be Point of X, y be Point of Y;
[y,x] in the carrier of [:Y,X:]; then
[y,x] in dom I by FUNCT_2:def 1;
hence (f*I).(y,x) = f.(I.(y,x)) by FUNCT_1:13
.= f.(x,y) by A1;
end;
theorem Th9:
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"
proof
let X,Y,Z be RealNormSpace,
f be PartFunc of Y,Z,
I be LinearOperator of X,Y,
V be Subset of Y;
assume that
A1: f is_differentiable_on V and
A2: I is one-to-one onto isometric;
A3: V is open by A1,NDIFF_1:32;
consider J be LinearOperator of Y,X such that
A4: J = I" & J is one-to-one onto isometric by A2,NDIFF_7:9;
A5: dom (f`| V) = V &
for x be Point of Y st x in V holds (f`| V)/.x = diff(f,x)
by A1,NDIFF_1:def 9;
set g = f*I;
set U = I"V;
A6: g is_differentiable_on U by A1,A2,NDIFF_7:29;
for y be Point of Y st y in dom (f`| V)
holds (f`| V).y = ((g`| U )/.(J.y)) *I"
proof
let y be Point of Y;
assume
A7: y in dom (f`| V); then
A8: (f`| V).y = (f`| V)/.y by PARTFUN1:def 6
.= diff(f,y) by A5,A7;
A9: f is_differentiable_in y by A1,A3,A5,A7,NDIFF_1:31;
consider x be Point of X such that
A10: y = I.x by A2,FUNCT_2:113;
reconsider I0 = I as Point of
R_NormSpace_of_BoundedLinearOperators(X,Y) by A2,LOPBAN_1:def 9;
A11: diff(f,y) * I0 * I0"
= modetrans(diff(f,y),Y,Z) * (modetrans(I0,X,Y) * I0") by RELAT_1:36
.= modetrans(diff(f,y),Y,Z) * (I * I") by LOPBAN_1:def 11
.= modetrans(diff(f,y),Y,Z) * (id rng I0) by A2,FUNCT_1:39
.= modetrans(diff(f,y),Y,Z) by A2,FUNCT_2:17
.= (f`| V).y by A8,LOPBAN_1:def 11;
x in U by A5,A10,A7,FUNCT_2:38; then
A12: ((g`|U)/.x) * I0" = diff(g,x) * I0" by A6,NDIFF_1:def 9;
x = J.y by A2,A4,A10,FUNCT_2:26;
hence (f`| V).y = ((g`| U )/.(J.y)) * I"
by A2,A9,A10,A11,A12,NDIFF_7:27;
end;
hence thesis by A4,A5;
end;
theorem Th10:
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)
proof
let X,Y,Z be RealNormSpace,
V be Subset of Y,
g be PartFunc of Y,Z,
I be LinearOperator of X,Y;
assume that
A1: I is one-to-one onto isometric and
A2: g is_differentiable_on V;
consider J be LinearOperator of Y,X such that
A3: J = I" & J is one-to-one onto isometric by A1,NDIFF_7:9;
set f = g * I;
set U = I"(V);
A4: dom J = the carrier of Y by FUNCT_2:def 1;
A5: f is_differentiable_on U by A1,A2,NDIFF_7:29;
A6: dom(f`|U) = U by A5,NDIFF_1:def 9;
A7: dom(g`|V) = V by A2,NDIFF_1:def 9;
set F = f`|U;
set G = g`|V;
A8: G is_continuous_on V implies F is_continuous_on U
proof
assume
A10: G is_continuous_on V;
for x0 be Point of X, e be Real st x0 in U & 0 < e
ex d be Real
st 0 < d
& for x1 be Point of X st x1 in U & ||. x1 - x0 .|| < d
holds ||. F/.x1 - F/.x0 .|| < e
proof
let x0 be Point of X,
e be Real;
assume
A11: x0 in U & 0 < e;
consider y0 be Point of Y such that
A12: x0 = J.y0 by A3,FUNCT_2:113;
A13: I.x0 = y0 by A1,A3,A12,FUNCT_1:35; then
A14: y0 in V by A11,FUNCT_2:38; then
consider d be Real such that
A15: 0 < d &
for y1 be Point of Y st y1 in V & ||. y1 - y0 .|| < d
holds ||. G/.y1 - G/.y0 .|| < e by A10,A11,NFCONT_1:19;
take d;
thus 0 < d by A15;
thus for x1 be Point of X st x1 in U & ||. x1 - x0 .|| < d
holds ||. F/.x1 - F/.x0 .|| < e
proof
let x1 be Point of X;
assume
A16: x1 in U & ||. x1 - x0 .|| < d;
consider y1 be Point of Y such that
A17: x1 = J.y1 by A3,FUNCT_2:113;
A18: I.x1 = y1 by A1,A3,A17,FUNCT_1:35; then
A19: y1 in V by A16,FUNCT_2:38;
||. y1 - y0 .|| = ||. x1 - x0 .|| by A1,A13,A18; then
A20: ||. G/.y1 - G/.y0 .|| < e by A15,A16,A19;
A21: G/.y1 = G.y1 by A7,A19,PARTFUN1:def 6
.= (F/.x1)*J by A1,A2,A3,A17,A19,Th9;
A22: G/.y0 = G.y0 by A7,A14,PARTFUN1:def 6
.= (F/.x0)*J by A1,A2,A3,A12,A14,Th9;
reconsider dF = F/.x1 - F/.x0
as Lipschitzian LinearOperator of X,Z by LOPBAN_1:def 9;
reconsider dG = G/.y1 - G/.y0
as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;
now
let v be VECTOR of Y;
A23: ((F/.x1 - F/.x0)*J).v
= (F/.x1 - F/.x0).(J.v) by A4,FUNCT_1:13
.= (F/.x1).(J.v) - (F/.x0).(J.v) by LOPBAN_1:40;
A24: (G/.y1).v = (F/.x1).(J.v) by A4,A21,FUNCT_1:13;
(G/.y0).v = (F/.x0).(J.v) by A4,A22,FUNCT_1:13;
hence (dF*J).v = dG.v by A23,A24,LOPBAN_1:40;
end; then
dF*J = dG;
hence ||. F/.x1 - F/.x0 .|| < e by A3,A20,NDIFF_7:22;
end;
end;
hence thesis by A6,NFCONT_1:19;
end;
F is_continuous_on U implies G is_continuous_on V
proof
assume
A25: F is_continuous_on U;
for y0 be Point of Y,e be Real st y0 in V & 0 < e
ex d be Real
st 0 < d
& for y1 be Point of Y st y1 in V & ||. y1 - y0 .|| < d
holds ||. G/.y1 - G/.y0 .|| < e
proof
let y0 be Point of Y,
e be Real;
assume
A26: y0 in V & 0<e;
set x0 = J.y0;
I.x0 = y0 by A1,A3,FUNCT_1:35; then
x0 in U by A26,FUNCT_2:38; then
consider d be Real such that
A27: 0 < d
& for x1 be Point of X st x1 in U & ||. x1 - x0 .|| < d
holds ||. F/.x1 - F/.x0 .|| < e by A25,A26,NFCONT_1:19;
take d;
thus 0 < d by A27;
let y1 be Point of Y;
assume
A28: y1 in V & ||. y1 - y0 .|| < d;
set x1 = J.y1;
I.x1 = y1 by A1,A3,FUNCT_1:35; then
A29: x1 in U by A28,FUNCT_2:38;
||. x1 - x0 .|| = ||. y1 - y0 .|| by A3; then
A30: ||. F/.x1 - F/.x0 .|| < e by A27,A28,A29;
A31: G/.y1 = G.y1 by A7,A28,PARTFUN1:def 6
.= (F/.x1)*J by A1,A2,A3,A28,Th9;
A32: G/.y0 = G.y0 by A7,A26,PARTFUN1:def 6
.= (F/.x0)*J by A1,A2,A3,A26,Th9;
reconsider dF = F/.x1 - F/.x0
as Lipschitzian LinearOperator of X,Z by LOPBAN_1:def 9;
reconsider dG = G/.y1 - G/.y0
as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;
now
let v be VECTOR of Y;
A33: ((F/.x1 - F/.x0)*J).v
= (F/.x1 - F/.x0).(J.v) by A4,FUNCT_1:13
.= (F/.x1).(J.v) - (F/.x0).(J.v) by LOPBAN_1:40;
A34: (G/.y1).v = (F/.x1).(J.v) by A4,A31,FUNCT_1:13;
(G/.y0).v = (F/.x0).(J.v) by A4,A32,FUNCT_1:13;
hence (dF*J).v = dG.v by A33,A34,LOPBAN_1:40;
end; then
dF*J = dG;
hence ||. G/.y1 - G/.y0 .|| < e by A3,A30,NDIFF_7:22;
end;
hence thesis by A7,NFCONT_1:19;
end;
hence thesis by A8;
end;
theorem Th11:
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)
proof
let 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:];
assume
A1: for y be Point of Y,x be Point of X
holds I.(y,x) = [x,y];
let a be Point of X, b be Point of Y,
u be Point of [:X,Y:],
v be Point of [:Y,X:];
assume
A2: u in U & u = [a,b] & v = [b,a];
A3: for x be object holds
x in dom(f * reproj1(u)) iff x in dom((f*I) * reproj2(v))
proof
let x be object;
A4: x in dom(f * reproj1(u))
iff x in dom reproj1(u) & (reproj1(u)).x in dom f by FUNCT_1:11;
A5: x in dom(f * reproj1(u)) implies x in dom((f*I) * reproj2(v))
proof
assume
A6: x in dom(f * reproj1(u)); then
A7: x in the carrier of X;
reconsider x as Point of X by A6;
A8: x in dom reproj2(v) by A7,FUNCT_2:def 1;
(reproj2(v)).x = [(v `1),x] by NDIFF_7:def 2
.= [b, x] by A2;
then
A9: I.((reproj2(v)).x) = I.(b,x)
.= [x,(u `2)] by A1,A2
.= (reproj1(u)).x by NDIFF_7:def 1;
(reproj2(v)).x in the carrier of [:Y,X:]; then
(reproj2(v)).x in dom I by FUNCT_2:def 1; then
(reproj2(v)).x in dom(f*I) by A4,A6,A9,FUNCT_1:11;
hence thesis by A8,FUNCT_1:11;
end;
x in dom((f*I) * reproj2(v)) implies x in dom(f * reproj1(u))
proof
assume
A10: x in dom ((f*I) * reproj2(v)); then
A11: x in dom reproj2(v)
& (reproj2(v)).x in dom(f*I) by FUNCT_1:11;
reconsider x as Point of X by A10;
(reproj2(v)).x = [(v `1),x] by NDIFF_7:def 2
.= [b, x] by A2;
then
I.( (reproj2(v)).x) = I.(b,x)
.= [x,(u `2)] by A1,A2
.= (reproj1(u)).x by NDIFF_7:def 1;
then
A12: (reproj1(u)).x in dom f by A11,FUNCT_1:11;
dom(reproj1(u)) = the carrier of X by FUNCT_2:def 1;
hence thesis by A12,FUNCT_1:11;
end;
hence thesis by A5;
end;
A13: for y be object holds
y in dom(f * reproj2(u)) iff y in dom((f*I) * reproj1(v))
proof
let y be object;
A14: y in dom(f * reproj2(u))
iff y in dom reproj2(u) & (reproj2(u)).y in dom f by FUNCT_1:11;
A15: y in dom(f * reproj2(u)) implies y in dom((f*I) * reproj1(v))
proof
assume
A16: y in dom(f * reproj2(u)); then
A17: y in the carrier of Y;
reconsider y as Point of Y by A16;
A18: y in dom reproj1(v) by A17,FUNCT_2:def 1;
(reproj1(v)).y = [y,(v `2)] by NDIFF_7:def 1
.= [y,a] by A2;
then
A19: I.((reproj1(v)).y) = I.(y,a)
.= [(u `1),y] by A1,A2
.= (reproj2(u)).y by NDIFF_7:def 2;
(reproj1(v)).y in the carrier of [:Y,X:]; then
(reproj1(v)).y in dom I by FUNCT_2:def 1; then
(reproj1(v)).y in dom(f*I) by A14,A16,A19,FUNCT_1:11;
hence thesis by A18,FUNCT_1:11;
end;
y in dom((f*I) * reproj1(v)) implies y in dom(f * reproj2(u))
proof
assume
A20: y in dom((f*I) * reproj1(v)); then
A21: y in dom reproj1(v) & (reproj1(v)).y in dom (f*I) by FUNCT_1:11;
reconsider y as Point of Y by A20;
(reproj1(v)).y = [y,(v `2)] by NDIFF_7:def 1
.= [y,a] by A2;
then
I.((reproj1(v)).y) = I.(y,a)
.= [(u `1),y] by A1,A2
.= (reproj2(u)).y by NDIFF_7:def 2;
then
A22: (reproj2(u)).y in dom f by A21,FUNCT_1:11;
dom(reproj2(u)) = the carrier of Y by FUNCT_2:def 1;
hence thesis by A22,FUNCT_1:11;
end;
hence thesis by A15;
end;
for x be object st x in dom(f * reproj1(u))
holds (f * reproj1(u)).x = ((f*I) * reproj2(v)).x
proof
let x be object;
assume
A23: x in dom(f * reproj1(u)); then
reconsider x as Point of X;
A24: (reproj1(u)).x = [x,(u`2)] by NDIFF_7:def 1
.= I.(b,x) by A1,A2
.= I.[v`1,x] by A2
.= I.((reproj2(v)).x) by NDIFF_7:def 2;
(reproj2(v)).x in the carrier of [:Y,X:]; then
A25: (reproj2(v)).x in dom I by FUNCT_2:def 1;
A26: dom(reproj2(v)) = the carrier of X by FUNCT_2:def 1;
(f * reproj1(u)).x
= f.(I.((reproj2(v)).x)) by A23,A24,FUNCT_1:12
.= (f*I).((reproj2(v)).x) by A25,FUNCT_1:13
.= ((f*I)*reproj2(v)).x by A26,FUNCT_1:13;
hence thesis;
end;
hence f * reproj1(u) = (f*I) * reproj2(v) by A3,FUNCT_1:2,TARSKI:2;
for y be object st y in dom(f * reproj2(u))
holds (f * reproj2(u)).y = ((f*I) * reproj1(v)).y
proof
let y be object;
assume
A27: y in dom(f * reproj2(u)); then
reconsider y as Point of Y;
A28: (reproj2(u)).y = [(u`1),y] by NDIFF_7:def 2
.= I.(y,a) by A1,A2
.= I.[y,v`2] by A2
.= I.((reproj1(v)).y) by NDIFF_7:def 1;
(reproj1(v)).y in the carrier of [:Y,X:]; then
A29: (reproj1(v)).y in dom I by FUNCT_2:def 1;
A30: dom(reproj1(v)) = the carrier of Y by FUNCT_2:def 1;
(f * reproj2(u)).y
= f.(I.((reproj1(v)).y)) by A27,A28,FUNCT_1:12
.= (f*I).((reproj1(v)).y) by A29,FUNCT_1:13
.= ((f*I) * reproj1(v)).y by A30,FUNCT_1:13;
hence thesis;
end;
hence f*reproj2(u) = (f*I)*reproj1(v) by A13,FUNCT_1:2,TARSKI:2;
end;
theorem
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 ) by Th11;
theorem
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) by Th11;
begin :: Application of implicit function theorem
theorem Th14:
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)
proof
let 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:];
assume that
A1: Z is open and
A2: dom f = Z and
A3: f is_differentiable_on Z and
A4: f `| Z is_continuous_on Z and
A5: [a,b] in Z and
A6: f.(a,b) = c and
A7: z = [a,b] and
A8: partdiff`1(f,z) is invertible;
set I = Exch(F,E);
A9: I is one-to-one onto isometric
& for s be Point of F,t be Point of E
holds I.(s,t) = [t,s] by Def1; then
consider J be LinearOperator of [:E,F:],[:F,E:] such that
A10: J = I" & J is one-to-one onto isometric by NDIFF_7:9;
set Z1 = J.:Z;
set f1 = f*I;
A11: Z1 is open by A1,A10,NDIFF_7:13;
A12: I"Z = Z1 by A9,A10,FUNCT_1:85;
A13: dom f1 = I" (dom f) by A9,Th8
.= Z1 by A2,A9,A10,FUNCT_1:85;
A14: f1 is_differentiable_on Z1 by A3,A9,A12,NDIFF_7:29;
reconsider z1 = [b,a] as Point of [:F,E:];
A16: f1 `| Z1 is_continuous_on Z1 by A3,A4,A9,A12,Th10;
A18: f1.(b,a) = c by A6,A9,Th8;
A19: partdiff`1(f,z) = partdiff`2(f1,z1) by A7,A9,Th11;
consider r2,r1 be Real such that
A20: 0 < r2 & 0 < r1
& [:Ball(b,r2),cl_Ball(a,r1):] c= Z1
& ( 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) & f1.(y,x) = 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)
& f1.(y,x1) =c & f1.(y,x2)= 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 f1.(y,g.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 [:F,E:]
st y in Ball(b,r2) & z = [y,g.y]
holds diff(g,y) = - ( Inv partdiff`2(f1,z)) * partdiff`1(f1,z) )
& ( for y be Point of F, z be Point of [:F,E:]
st y in Ball(b,r2) & z = [y,g.y]
holds partdiff`2(f1,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 f1.(y,g1.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 f1.(y,g2.y) = c )
holds g1 = g2)
by A5,A8,A11,A12,A13,A14,A16,A18,A19,Th7,NDIFF_9:21;
take r1,r2;
thus 0 < r1 & 0 < r2 by A20;
for s be object
st s in [:cl_Ball(a,r1),Ball(b,r2):]
holds s in Z
proof
let s be object;
assume s in [:cl_Ball(a,r1),Ball(b,r2):]; then
consider x,y be object such that
A22: x in cl_Ball(a,r1) & y in Ball(b,r2)
& s = [x,y] by ZFMISC_1:def 2;
[y,x] in [:Ball(b,r2),cl_Ball(a,r1):] by A22,ZFMISC_1:def 2;
hence s in Z by A12,A20,A22,Th7;
end;
hence [:cl_Ball(a,r1),Ball(b,r2):] c= Z;
thus 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
proof
let y be Point of F;
assume y in Ball(b,r2); then
consider x be Point of E such that
A26: x in Ball(a,r1) & f1.(y,x) = c by A20;
take x;
thus x in Ball(a,r1) by A26;
thus f.(x,y) = c by A9,A26,Th8;
end;
thus 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
proof
let y be Point of F;
assume
A27: y in Ball(b,r2);
let x1,x2 be Point of E;
assume
A28: x1 in Ball(a,r1) & x2 in Ball(a,r1)
& f.(x1,y) = c & f.(x2,y) = c;
A29: f1.(y,x1) = f.(x1,y) by A9,Th8;
f1.(y,x2) = f.(x2,y) by A9,Th8;
hence x1 = x2 by A20,A27,A28,A29;
end;
thus 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 )
proof
consider g be PartFunc of F,E such that
A30: 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 f1.(y,g.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 [:F,E:]
st y in Ball(b,r2) & z = [y,g.y]
holds diff(g,y) = - ( Inv partdiff`2(f1,z)) * partdiff`1(f1,z) )
& ( for y be Point of F, z be Point of [:F,E:]
st y in Ball(b,r2) & z = [y,g.y]
holds partdiff`2(f1,z) is invertible ) by A20;
take g;
thus dom g = Ball(b,r2) & rng g c= Ball(a,r1)
& g is_continuous_on Ball(b,r2)
& g.b = a by A30;
thus for y be Point of F st y in Ball(b,r2)
holds f.(g.y,y) = c
proof
let y be Point of F;
assume
A31: y in Ball(b,r2); then
A32:f1.(y,g.y) = c by A30;
g.y in rng g by A30,A31,FUNCT_1:3;
hence thesis by A9,A32,Th8;
end;
thus g is_differentiable_on Ball(b,r2)
& g `| Ball(b,r2) is_continuous_on Ball(b,r2) by A30;
thus 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)
proof
let y be Point of F, z be Point of [:E,F:];
assume
A33: y in Ball(b,r2) & z = [g.y,y]; then
g.y in rng g by A30,FUNCT_1:3; then
reconsider x = g.y as Point of E;
reconsider z0 = [y,x] as Point of [:F,E:];
partdiff`1(f,z) = partdiff`2(f1,z0)
& partdiff`2(f,z) = partdiff`1(f1,z0) by A9,A33,Th11;
hence diff(g,y) = - (Inv partdiff`1(f,z)) * partdiff`2(f,z)
by A30,A33;
end;
thus 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
proof
let y be Point of F, z be Point of [:E,F:];
assume
A37: y in Ball(b,r2) & z = [g.y,y]; then
g.y in rng g by A30,FUNCT_1:3; then
reconsider x = g.y as Point of E;
reconsider z0 = [y,x] as Point of [:F,E:];
partdiff`1(f,z) = partdiff`2(f1,z0)
& partdiff`2(f,z) = partdiff`1(f1,z0) by A9,A37,Th11;
hence partdiff`1(f,z) is invertible by A30,A37;
end;
end;
thus 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
proof
let g1,g2 be PartFunc of F,E;
assume
A41: 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 );
A42: for y be Point of F st y in Ball(b,r2)
holds f1.(y,g1.y) = c
proof
let y be Point of F;
assume
A43: y in Ball(b,r2); then
A44: f.(g1.y,y) = c by A41;
g1.y in rng g1 by A41,A43,FUNCT_1:3;
hence thesis by A9,A44,Th8;
end;
for y be Point of F st y in Ball(b,r2)
holds f1.(y,g2.y) = c
proof
let y be Point of F;
assume
A45: y in Ball(b,r2); then
A46: f.(g2.y,y) = c by A41;
g2.y in rng g2 by A41,A45,FUNCT_1:3;
hence thesis by A9,A46,Th8;
end;
hence g1 = g2 by A20,A41,A42;
end;
end;
theorem Th15:
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
proof
let 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:];
assume that
A1: D is open and
A2: dom f = D & D <> {} and
A3: f is_differentiable_on D and
A4: f `| D is_continuous_on D and
A5: Z = [:D,the carrier of F:] and
A6: dom f1 = Z and
A7: for s be Point of E,
t be Point of F
st s in D
holds f1.(s,t) = f/.s - t;
A9: Z is open by A1,A5,Th4;
A10: for z being Point of [:E,F:] st z in Z holds
f1 is_partial_differentiable_in`1 z
& partdiff`1(f1,z) = diff(f,z `1)
proof
let z be Point of [:E,F:];
assume
A11: z in Z;
consider x be Point of E,y be Point of F such that
A12: z = [x,y] by PRVECT_3:18;
set CST = D --> y;
A13: rng CST = {y} & dom CST = D by A2,FUNCOP_1:8,13; then
reconsider CST as PartFunc of E,F by RELSET_1:4;
A14: CST is_differentiable_on D
& for s being Point of E st s in D holds
(CST `| D) /. s = 0.(R_NormSpace_of_BoundedLinearOperators(E,F))
by A1,A13,NDIFF_1:33;
A16: dom(f-CST) = D /\ D by A2,A13,VFUNCT_1:def 2
.= D;
A17: for s be object holds
s in dom(f1 * reproj1(z)) iff s in dom(f-CST)
proof
let s be object;
hereby
assume
A19: s in dom(f1*reproj1(z)); then
reconsider t = s as Point of E;
(reproj1(z)).t = [t, z`2] by NDIFF_7:def 1
.= [t, y] by A12; then
[t,y] in dom f1 by A19,FUNCT_1:11;
hence s in dom(f-CST) by A5,A6,A16,ZFMISC_1:87;
end;
assume
A20: s in dom (f-CST); then
reconsider t = s as Point of E;
(reproj1(z)).t = [t, z`2] by NDIFF_7:def 1
.= [t, y] by A12; then
A23: (reproj1(z)).t in dom f1 by A5,A6,A16,A20,ZFMISC_1:87;
dom(reproj1(z)) = the carrier of E by FUNCT_2:def 1;
hence s in dom(f1 * reproj1(z)) by A23,FUNCT_1:11;
end;
A24: for s be object
st s in dom(f1 * reproj1(z))
holds (f1 * reproj1(z)).s = (f-CST).s
proof
let s be object;
assume
A25: s in dom(f1 * reproj1(z)); then
A26: s in dom (reproj1(z))
& (reproj1(z)).s in dom f1 by FUNCT_1:11;
reconsider t = s as Point of E by A25;
A27: (reproj1(z)).t = [t, (z`2)] by NDIFF_7:def 1
.= [t, y] by A12; then
A28: t in D by A5,A6,A26,ZFMISC_1:87; then
A29: CST/.s = CST.s by A13,PARTFUN1:def 6
.= y by A28,FUNCOP_1:7;
thus (f1 * reproj1(z)).s = f1.(t,y) by A25,A27,FUNCT_1:12
.= f/.t - CST/.s by A7,A28,A29
.= (f-CST)/.s by A17,A25,VFUNCT_1:def 2
.= (f-CST).s by A17,A25,PARTFUN1:def 6;
end;
A32: x in D by A5,A11,A12,ZFMISC_1:87; then
A33: f is_differentiable_in x by A1,A3,NDIFF_1:31;
CST is_differentiable_in x by A1,A14,A32,NDIFF_1:31; then
A34: f-CST is_differentiable_in x
& diff(f-CST,x) = diff(f,x) - diff(CST,x) by A33,NDIFF_1:36;
hence f1 is_partial_differentiable_in`1 z
by A12,A17,A24,FUNCT_1:2,TARSKI:2;
A36: diff(CST,x)
= (CST `| D) /. x by A14,A32,NDIFF_1:def 9
.= 0. (R_NormSpace_of_BoundedLinearOperators (E,F))
by A1,A13,A32,NDIFF_1:33;
thus partdiff`1 (f1,z)
= diff(f-CST,x) by A12,A17,A24,FUNCT_1:2,TARSKI:2
.= diff(f,z `1) by A12,A34,A36,RLVECT_1:13;
end; then
A37: f1 is_partial_differentiable_on`1 Z by A6; then
A38: Z = dom (f1 `partial`1| Z) by NDIFF_7:def 10;
for x0 being Point of [:E,F:]
for r being Real st x0 in Z & 0 < r holds
ex s being Real
st 0 < s
& for x1 being Point of [:E,F:]
st x1 in Z & ||.(x1 - x0).|| < s
holds ||.(f1 `partial`1| Z) /. x1 - (f1 `partial`1| Z) /. x0.|| < r
proof
let x0 be Point of [:E,F:];
let r be Real;
assume
A39: x0 in Z & 0 < r;
consider s0 be Point of E,t0 be Point of F such that
A40: x0 = [s0,t0] by PRVECT_3:18;
A41: s0 in D by A5,A39,A40,ZFMISC_1:87; then
consider s being Real such that
A43: 0 < s
& for s1 being Point of E
st s1 in D & ||.s1 - s0.|| < s
holds ||.(f `| D) /. s1 - (f `| D) /. s0.|| < r
by A4,A39,NFCONT_1:19;
take s;
thus 0 < s by A43;
let x1 be Point of [:E,F:];
assume
A44: x1 in Z & ||.x1 - x0.|| < s;
consider s1 be Point of E,t1 be Point of F such that
A45: x1 = [s1,t1] by PRVECT_3:18;
A46: s1 in D by A5,A44,A45,ZFMISC_1:87;
-x0 = [-s0,-t0] by A40,PRVECT_3:18; then
x1 - x0 = [s1-s0,t1-t0] by A45,PRVECT_3:18; then
||.s1 - s0.|| <= ||.x1-x0.|| by LOPBAN_7:15; then
A48: ||.s1 - s0.|| < s by A44,XXREAL_0:2;
A49: (f `| D) /. s1 = diff(f,x1 `1) by A3,A45,A46,NDIFF_1:def 9
.= partdiff`1 (f1,x1) by A10,A44
.= (f1 `partial`1| Z) /. x1 by A37,A44,NDIFF_7:def 10;
(f `| D) /. s0 = diff(f,x0 `1) by A3,A40,A41,NDIFF_1:def 9
.= partdiff`1 (f1,x0) by A10,A39
.= (f1 `partial`1| Z) /. x0 by A37,A39,NDIFF_7:def 10;
hence ||.(f1 `partial`1| Z) /. x1 - (f1 `partial`1| Z) /. x0.|| < r
by A43,A46,A48,A49;
end; then
A50: f1 `partial`1| Z is_continuous_on Z by A38,NFCONT_1:19;
reconsider J = (FuncUnit F)
as Point of R_NormSpace_of_BoundedLinearOperators (F,F);
A51: for z being Point of [:E,F:] st z in Z holds
f1 is_partial_differentiable_in`2 z
& partdiff`2(f1,z) = - J
proof
let z be Point of [:E,F:];
assume
A52: z in Z;
the carrier of F c= the carrier of F; then
reconsider CF = the carrier of F as Subset of F;
for y be Point of F st y in CF
ex r be Real st 0 < r & Ball(y,r) c= CF
proof
let y be Point of F;
assume y in CF;
take r=1;
thus 0 < r;
thus Ball(y,r) c= CF;
end; then
A53: CF is open by NDIFF_8:20;
consider x be Point of E,y be Point of F such that
A54: z = [x,y] by PRVECT_3:18;
A55: x in D by A5,A52,A54,ZFMISC_1:87;
set fx = ((CF) --> f/.x );
A57: rng fx = {f/.x} & dom fx = CF by FUNCOP_1:8,FUNCOP_1:13;
reconsider fx as PartFunc of F,F;
A58: fx is_differentiable_on CF
& for s being Point of F st s in CF holds
(fx `| CF) /. s = 0. (R_NormSpace_of_BoundedLinearOperators(F,F))
by A53,A57,NDIFF_1:33;
set I = id CF;
A59: dom I = CF & rng I = CF;
A60: I | CF = I;
reconsider I as PartFunc of F,F;
A61: I is_differentiable_on(CF)
& for s being Point of F st s in CF holds
(I `| CF ) /. s = id CF by A53,A59,A60,NDIFF_1:38;
dom(fx-I) = (dom fx) /\ (dom I)
& for s being Element of F st s in dom(fx-I) holds
(fx-I) /. s = (fx /. s) - (I /. s) by VFUNCT_1:def 2;
then
A63: dom (fx-I) = CF /\ CF by FUNCOP_1:13
.= CF;
A64: for s be object holds
s in dom(f1 * reproj2(z)) iff s in dom(fx-I)
proof
let s be object;
A66: s in dom(f1 * reproj2(z))
iff s in dom reproj2(z) & (reproj2(z)).s in dom f1 by FUNCT_1:11;
thus s in dom(f1 * reproj2(z)) implies s in dom(fx-I) by A63;
assume s in dom (fx-I); then
reconsider t = s as Point of F;
A69: (reproj2(z)).t = [z`1, t] by NDIFF_7:def 2
.= [x, t] by A54;
dom(reproj2(z)) = the carrier of F by FUNCT_2:def 1;
hence s in dom(f1 * reproj2(z)) by A5,A6,A55,A66,A69,ZFMISC_1:87;
end;
A71: for s be object
st s in dom(f1 * reproj2(z))
holds (f1 * reproj2(z)).s = (fx-I).s
proof
let s be object;
assume
A72: s in dom(f1 * reproj2(z)); then
reconsider t = s as Point of F;
A73: (reproj2(z)).t = [z`1, t] by NDIFF_7:def 2
.= [x, t] by A54;
A74: t in CF; then
A75: I/.s = I.s by A59,PARTFUN1:def 6
.= s by A74;
A76: fx/.s = fx.s by A57,A74,PARTFUN1:def 6
.= f/.x by A74,FUNCOP_1:7;
thus (f1*reproj2(z)).s = f1.(x,t) by A72,A73,FUNCT_1:12
.= f/.x - I/.s by A7,A55,A75
.= (fx-I)/.s by A64,A72,A76,VFUNCT_1:def 2
.= (fx-I).s by A64,A72,PARTFUN1:def 6;
end;
A79: fx is_differentiable_in y by A53,A58,NDIFF_1:31;
I is_differentiable_in y by A53,A61,NDIFF_1:31; then
A80: fx-I is_differentiable_in y
& diff(fx-I,y) = diff(fx,y) - diff(I,y) by A79,NDIFF_1:36;
hence f1 is_partial_differentiable_in`2 z
by A54,A64,A71,FUNCT_1:2,TARSKI:2;
A82: diff(I,y) = (I `| CF) /. y by A61,NDIFF_1:def 9
.= J by A53,A59,A60,NDIFF_1:38;
diff(fx,y) = (fx `| (CF)) /. y by A58,NDIFF_1:def 9
.= 0.(R_NormSpace_of_BoundedLinearOperators(F,F))
by A53,A57,NDIFF_1:33; then
diff(fx-I,y) = -J by A80,A82,RLVECT_1:14;
hence partdiff`2(f1,z) = - J by A54,A64,A71,FUNCT_1:2,TARSKI:2;
end; then
A84: f1 is_partial_differentiable_on`2 Z by A6; then
A85: Z = dom (f1 `partial`2| Z) by NDIFF_7:def 11;
for x0 being Point of [:E,F:]
for r being Real st x0 in Z & 0 < r
holds
ex s being Real
st 0 < s
& for x1 being Point of [:E,F:]
st x1 in Z & ||.(x1 - x0).|| < s
holds ||.(f1 `partial`2| Z) /. x1
- (f1 `partial`2| Z) /. x0.|| < r
proof
let x0 be Point of [:E,F:];
let r be Real;
assume
A86: x0 in Z & 0 < r;
take s = 1;
thus 0 < s;
let x1 be Point of [:E,F:];
assume
A88: x1 in Z & ||.x1 - x0.|| < s;
A90: -J = partdiff`2 (f1,x1) by A51,A88
.= (f1 `partial`2| Z) /. x1 by A84,A88,NDIFF_7:def 11;
-J = partdiff`2 (f1,x0) by A51,A86
.= (f1 `partial`2| Z) /. x0 by A84,A86,NDIFF_7:def 11; then
(f1 `partial`2| Z) /. x1 - (f1 `partial`2| Z) /. x0
= 0. (R_NormSpace_of_BoundedLinearOperators (F,F))
by A90,RLVECT_1:15;
hence ||.(f1 `partial`2| Z) /. x1
- (f1 `partial`2| Z) /. x0.|| < r
by A86,NORMSP_0:def 6;
end; then
f1 `partial`2| Z is_continuous_on Z by A85,NFCONT_1:19;
hence f1 is_differentiable_on Z
& f1 `| Z is_continuous_on Z by A9,A37,A50,A84,NDIFF_7:52;
thus 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
proof
let x be Point of E,y be Point of F,
z be Point of [:E,F:];
assume
A92: x in D & z = [x,y]; then
A93: z in Z by A5,ZFMISC_1:87;
take J;
thus J = id(the carrier of F);
thus partdiff`1 (f1,z) = diff(f,x) by A10,A92,A93;
thus partdiff`2 (f1,z) = -J by A51,A93;
end;
end;
theorem Th16:
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 )
proof
let E,F be non trivial RealBanachSpace,
D be Subset of E,
f be PartFunc of E,F,
a be Point of E,
b be Point of F;
assume that
A1: D is open and
A2: dom f = D and
A3: f is_differentiable_on D and
A4: f `| D is_continuous_on D and
A5: a in D and
A6: f.a = b and
A7: diff(f,a) is invertible;
reconsider Z = [:D,the carrier of F:]
as Subset of [:E,F:] by ZFMISC_1:96;
A9: Z is open by A1,Th4;
defpred P1[ object , object ]
means
ex x be Point of E,y be Point of F
st $1 = [x,y] & $2 = f/.x-y;
A10: for z being object st z in Z holds
ex y being object
st y in the carrier of F & P1[z,y]
proof
let z be object;
assume z in Z; then
consider x be Point of E, y be Point of F such that
A11: z = [x,y] by PRVECT_3:18;
take w = f/.x-y;
thus thesis by A11;
end;
consider f1 being Function of Z,the carrier of F such that
A12: for x being object st x in Z holds
P1[x,f1.x] from FUNCT_2:sch 1(A10);
A13: dom f1 = Z by FUNCT_2:def 1; then
dom f1 c= the carrier of [:E,F:]
& rng f1 c= the carrier of F; then
reconsider f1 as PartFunc of [:E,F:],F by RELSET_1:4;
A14: for s be Point of E,
t be Point of F
st s in D
holds f1.(s,t) = f/.s - t
proof
let s be Point of E,
t be Point of F;
assume s in D; then
consider x be Point of E,y be Point of F such that
A15: [s,t] = [x,y] & f1.[s,t] = f/.x-y by A12,ZFMISC_1:87;
s = x & t = y by A15,XTUPLE_0:1;
hence f1.(s,t) = f/.s-t by A15;
end;
reconsider z = [a,b] as Point of [:E,F:];
A16: f1 is_differentiable_on Z by A1,A2,A3,A4,A5,A13,A14,Th15;
A17: f1 `| Z is_continuous_on Z by A1,A2,A3,A4,A5,A13,A14,Th15;
f.a = f/.a by A2,A5,PARTFUN1:def 6; then
f/.a - b = 0.F by A6,RLVECT_1:15; then
A19: f1.(a,b) = 0.F by A5,A14;
ex J be Point of R_NormSpace_of_BoundedLinearOperators(F,F)
st J = id the carrier of F
& partdiff`1(f1,z) = diff(f,a)
& partdiff`2(f1,z) = -J
by A1,A2,A3,A4,A5,A13,A14,Th15; then
consider r1,r2 be Real such that
A21: 0 < r1 & 0 < r2
& [:cl_Ball(a,r1),Ball(b,r2):] c= Z
& ( for x be Point of F st x in Ball(b,r2) holds
ex y be Point of E
st y in Ball(a,r1) & f1.(y,x) = 0.F )
& ( for x be Point of F st x in Ball(b,r2) holds
for y1,y2 be Point of E
st y1 in Ball(a,r1) & y2 in Ball(a,r1)
& f1.(y1,x) = 0.F & f1.(y2,x) = 0.F
holds y1 = y2 )
& ( 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 x be Point of F st x in Ball(b,r2)
holds f1.(g.x,x) = 0.F )
& 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(f1,z)) * partdiff`2(f1,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(f1,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 f1.(g1.y,y) = 0.F )
& dom g2 = Ball(b,r2)
& rng g2 c= Ball(a,r1)
& ( for y be Point of F st y in Ball(b,r2)
holds f1.(g2.y,y) = 0.F )
holds g1 = g2)
by A5,A7,A9,A13,A16,A17,A19,Th14,ZFMISC_1:87;
take r1,r2;
thus 0 < r1 & 0 < r2 by A21;
for s be object st s in cl_Ball(a,r1) holds s in D
proof
let s be object;
assume
A23: s in cl_Ball(a,r1);
b in Ball(b,r2) by A21,NDIFF_8:13; then
[s,b] in [:cl_Ball(a,r1),Ball(b,r2):] by A23,ZFMISC_1:87;
hence s in D by A21,ZFMISC_1:87;
end;
hence
A24: cl_Ball(a,r1) c= D by TARSKI:def 3;
Ball(a,r1) c= cl_Ball(a,r1) by NDIFF_8:15; then
A25: Ball(a,r1) c= D by A24,XBOOLE_1:1;
thus 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
proof
let y be Point of F;
assume y in Ball(b,r2); then
consider x be Point of E such that
A26: x in Ball(a,r1) & f1.(x,y) = 0.F by A21;
take x;
f/.x - y = 0.F by A14,A25,A26;
hence thesis by A26,RLVECT_1:21;
end;
thus 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
proof
let y be Point of F;
assume
A27: y in Ball(b,r2);
let x1,x2 be Point of E;
assume
A28: x1 in Ball(a,r1) & x2 in Ball(a,r1)
& f/.x1 = y & f/.x2 = y; then
f/.x1 - y = 0.F & f/.x2 - y = 0.F by RLVECT_1:15; then
f1.(x1,y) = 0.F & f1.(x2,y) = 0.F by A14,A25,A28;
hence x1 = x2 by A21,A27,A28;
end;
thus 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 )
proof
consider g be PartFunc of F,E such that
A29: 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 f1.(g.y,y) = 0.F )
& ( 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(f1,z)) * partdiff`2(f1,z) )
& 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(f1,z)) * partdiff`2(f1,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(f1,z) is invertible ) by A21;
take g;
thus dom g = Ball(b,r2) & rng g c= Ball(a,r1) by A29;
thus g is_continuous_on Ball(b,r2) & g.b = a by A29;
thus for y be Point of F st y in Ball(b,r2)
holds f/.(g/.y) = y
proof
let y be Point of F;
assume
A30: y in Ball(b,r2); then
A31: f1.(g.y,y) = 0.F by A29;
g.y in rng g by A29,A30,FUNCT_1:3; then
g.y in Ball(a,r1) by A29; then
A32: f/.(g.y) -y = 0.F by A14,A25,A31;
g.y = g/.y by A29,A30,PARTFUN1:def 6;
hence f/.(g/.y) = y by A32,RLVECT_1:21;
end;
thus g is_differentiable_on Ball(b,r2)
& g `| Ball(b,r2) is_continuous_on Ball(b,r2) by A29;
thus for y be Point of F
st y in Ball(b,r2)
holds diff(g,y) = Inv diff(f,g/.y)
proof
let y be Point of F;
assume
A33: y in Ball(b,r2);
[g/.y,y] is set; then
reconsider z = [g.y,y] as Point of [:E,F:]
by A29,A33,PARTFUN1:def 6;
g.y in rng g by A29,A33,FUNCT_1:3; then
A34: g.y in Ball(a,r1) by A29;
g.y = g/.y by A29,A33,PARTFUN1:def 6; then
consider J be Point of R_NormSpace_of_BoundedLinearOperators(F,F)
such that
A35: J = id the carrier of F
& partdiff`1(f1,z) = diff(f,g/.y)
& partdiff`2(f1,z) = -J
by A1,A2,A3,A4,A13,A14,A25,A34,Th15;
thus diff(g,y)
= -(Inv partdiff`1(f1,z)) * partdiff`2(f1,z) by A29,A33
.= (-(Inv diff(f,g/.y))) * (-J) by A35,LOPBAN13:26
.= (Inv diff(f,g/.y)) * J by LOPBAN13:27
.= modetrans(Inv diff(f,g/.y),F,E) * (id the carrier of F)
by A35,LOPBAN_1:def 11
.= modetrans(Inv diff(f,g/.y),F,E) by FUNCT_2:17
.= Inv diff(f,g/.y) by LOPBAN_1:def 11;
end;
thus for y be Point of F
st y in Ball(b,r2)
holds diff(f,g/.y) is invertible
proof
let y be Point of F;
assume
A36: y in Ball(b,r2);
[g/.y,y] is set; then
reconsider z = [g.y,y] as Point of [:E,F:]
by A29,A36,PARTFUN1:def 6;
g.y in rng g by A29,A36,FUNCT_1:3; then
A38: g.y in Ball(a,r1) by A29;
g.y = g/.y by A29,A36,PARTFUN1:def 6; then
ex J be Point of R_NormSpace_of_BoundedLinearOperators(F,F)
st J = id the carrier of F
& partdiff`1(f1,z) = diff(f,g/.y)
& partdiff`2(f1,z) = -J
by A1,A2,A3,A4,A13,A14,A25,A38,Th15;
hence diff(f,g/.y) is invertible by A29,A36;
end;
end;
thus 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
proof
let g1,g2 be PartFunc of F,E;
assume
A40: 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 );
A41: for y be Point of F st y in Ball(b,r2)
holds f1.(g1.y,y) = 0.F
proof
let y be Point of F;
assume
A42: y in Ball(b,r2); then
g1.y in rng g1 by A40,FUNCT_1:3; then
g1.y in Ball(a,r1) by A40; then
A43: f1.(g1.y,y) = f/.(g1.y) - y by A14,A25;
f/.(g1.y) = y by A40,A42;
hence f1.(g1.y,y) = 0.F by A43,RLVECT_1:15;
end;
for y be Point of F st y in Ball(b,r2)
holds f1.(g2.y,y) = 0.F
proof
let y be Point of F;
assume
A45: y in Ball(b,r2); then
g2.y in rng g2 by A40,FUNCT_1:3; then
g2.y in Ball(a,r1) by A40; then
A46: f1.(g2.y,y) = f/.(g2.y) - y by A14,A25;
f/.(g2.y) = y by A40,A45;
hence f1.(g2.y,y) = 0.F by A46,RLVECT_1:15;
end;
hence g1 = g2 by A21,A40,A41;
end;
end;
begin :: Inverse function theorem for class C^1 functions
theorem Th17:
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) )
proof
let 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;
assume
A1: 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;
then consider r1,r2 be Real such that
A2: 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 ) by Th16;
consider Invf be PartFunc of F,E such that
A3: dom Invf = Ball(b,r2) & rng Invf c= Ball(a,r1)
& Invf is_continuous_on Ball(b,r2)
& Invf.b = a
& ( for y be Point of F st y in Ball(b,r2)
holds f/.(Invf/.y) = y )
& Invf is_differentiable_on Ball(b,r2)
& Invf `| Ball(b,r2) is_continuous_on Ball(b,r2)
& ( for y be Point of F
st y in Ball(b,r2)
holds diff(Invf,y) = Inv diff(f,Invf/.y) )
& ( for y be Point of F
st y in Ball(b,r2)
holds diff(f,Invf/.y) is invertible ) by A2;
A4: Ball(a,r1) c= cl_Ball(a,r1) by NDIFF_8:15;
set B = Ball(b,r2);
set A = Ball(a,r1) /\ (f"B);
A7: a in Ball(a,r1) by A2,NDIFF_8:13;
f.a in B by A1,A2,NDIFF_8:13; then
A9: a in (f"B) by A1,FUNCT_1:def 7;
for s be object st s in B holds s in f.:Ball(a,r1)
proof
let s be object;
assume
A10: s in B; then
reconsider s0 = s as Point of F;
A11: f/.(Invf/.s0) = s0 by A3,A10;
Invf/.s0 = Invf.s0 by A3,A10,PARTFUN1:def 6; then
A12: Invf/.s0 in rng Invf by A3,A10,FUNCT_1:3; then
Invf/.s0 in Ball(a,r1) by A3; then
B12: Invf/.s0 in cl_Ball(a,r1) by A4; then
f/.(Invf/.s0) = f.(Invf/.s0) by A1,A2,PARTFUN1:def 6;
hence s in f.:Ball(a,r1) by A1,A2,A3,A11,A12,B12,FUNCT_1:def 6;
end; then
A14: B c= f.:Ball(a,r1) by TARSKI:def 3;
A16: (f"B) is open by A1,NDIFF_1:45,Th1;
B16: for s be object holds s in f.:A iff s in B
proof
let s be object;
hereby
assume s in f.:A; then
consider x be object such that
A17: x in dom f & x in A & s = f.x by FUNCT_1:def 6;
x in (f"B) by A17,XBOOLE_0:def 4;
hence s in B by A17,FUNCT_1:def 7;
end;
assume
A18: s in B; then
consider x be object such that
A19: x in dom f & x in Ball(a,r1) & s = f.x by A14,FUNCT_1:def 6;
x in f"B by A18,A19,FUNCT_1:def 7; then
x in dom f & x in A & s=f.x by A19,XBOOLE_0:def 4;
hence s in f.:A by FUNCT_1:def 6;
end;
A21: rng (f|A) = f.:A by RELAT_1:115
.= B by B16,TARSKI:2;
A22: A c= Ball(a,r1) by XBOOLE_1:17; then
B22: A c= cl_Ball(a,r1) by A4,XBOOLE_1:1; then
A23: A c= dom f by A1,A2,XBOOLE_1:1;
A24: dom (f|A) = A by A1,A2,B22,RELAT_1:62,XBOOLE_1:1;
for y1,y2 be object
st y1 in dom (Invf) & y2 in dom (Invf) & (Invf).y1 = (Invf).y2
holds y1 = y2
proof
let y1,y2 be object;
assume
A25: y1 in dom (Invf) & y2 in dom (Invf)
& (Invf).y1 = (Invf).y2;
hence y1 = f/.((Invf)/.y1) by A3
.= f/.((Invf).y2) by A25,PARTFUN1:def 6
.= f/.((Invf)/.y2) by A25,PARTFUN1:def 6
.= y2 by A3,A25;
end; then
A27: Invf is one-to-one by FUNCT_1:def 4;
B27: for x1,x2 be object
st x1 in dom (f|A) & x2 in dom (f|A) & (f|A).x1 = (f|A).x2
holds x1 = x2
proof
let x1,x2 be object;
assume
A28: x1 in dom (f|A)
& x2 in dom (f|A)
& (f|A).x1 =(f|A).x2; then
A29: f.x1 = (f|A).x2 by FUNCT_1:47
.= f.x2 by A28,FUNCT_1:47;
x1 in (f"B) by A28,XBOOLE_0:def 4; then
A31: x1 in dom f & f.x1 in B by FUNCT_1:def 7;
x2 in (f"B) by A28,XBOOLE_0:def 4; then
A33: x2 in dom f & f.x2 in B by FUNCT_1:def 7;
A34: f/.x1 = f.x2 by A29,A31,PARTFUN1:def 6
.= f/.x2 by A33,PARTFUN1:def 6;
A35: f/.x1 in B & f/.x2 in B by A31,A33,PARTFUN1:def 6;
x1 in Ball(a,r1) & x2 in Ball(a,r1) by A28,XBOOLE_0:def 4;
hence x1 = x2 by A2,A34,A35;
end; then
A36:f|A is one-to-one by FUNCT_1:def 4; then
A37: dom ((f|A)") = B by A21,FUNCT_1:33;
for x be object st x in dom ((f|A)") holds (f|A)".x = Invf.x
proof
let x be object;
assume
A39: x in dom ((f|A)"); then
reconsider y = x as Point of F by A37;
A41: y = f/.((Invf)/.y) by A3,A37,A39
.= f/.((Invf).y) by A3,A37,A39,PARTFUN1:def 6;
(f|A)".y in rng ((f|A)") by A39,FUNCT_1:3; then
A42: (f|A)".y in A by A24,A36,FUNCT_1:33;
A44: y = (f|A).((f|A)".y) by A21,A36,A37,A39,FUNCT_1:35
.= f.((f|A)".y) by A42,FUNCT_1:49
.= f/.((f|A)".y) by A23,A42,PARTFUN1:def 6;
(Invf).y in rng Invf by A3,A37,A39,FUNCT_1:3;
hence thesis by A2,A3,A22,A37,A39,A41,A42,A44;
end; then
A47: (f|A)" = Invf by A3,A37,FUNCT_1:2;
A49: rng Invf = dom((Invf)") by A27,FUNCT_1:33
.= dom(f|A) by B27,A47,FUNCT_1:43,def 4
.= A by A1,A2,B22,RELAT_1:62,XBOOLE_1:1;
take A,B,Invf;
thus thesis by A1,A2,A3,A7,A9,A16,B16,A21,B22,A36,A47,A49,
FUNCT_1:43,NDIFF_8:13,RELAT_1:62,TARSKI:2,XBOOLE_0:def 4,
XBOOLE_1:1;
end;
theorem Th18:
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) )
proof
let 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;
assume
A1: 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;
then
consider A be Subset of E,B be Subset of F,
g be PartFunc of F,E such that
A2: 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) ) by Th17;
let r1 be Real;
assume
A3: 0 < r1;
A5: g"Ball(a,r1) = (f|A).:(Ball(a,r1)) by A2,FUNCT_1:85;
A6: (f|A).:(Ball(a,r1)) c= f.:(Ball(a,r1)) by RELAT_1:128;
a in dom (f|A) & a in Ball(a,r1) & f.a = (f|A).a
by A2,A3,FUNCT_1:49,NDIFF_8:13; then
f.a in (f|A).:(Ball(a,r1)) by FUNCT_1:def 6;
then
consider r2 be Real such that
A7: 0 < r2 & Ball(b,r2) c= (f|A).:(Ball(a,r1))
by A1,A2,A5,Th1,NDIFF_8:20;
thus thesis by A6,A7,XBOOLE_1:1;
end;
theorem
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
proof
let E,F be non trivial RealBanachSpace,
Z be Subset of E,
f be PartFunc of E,F;
assume
A1: Z is open & dom f = Z
& f is_differentiable_on Z
& f `| Z is_continuous_on Z;
assume
A2: for x be Point of E st x in Z
holds diff(f,x) is invertible;
thus
A3: 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)
proof
let x be Point of E,r1 be Real;
assume
A4: x in Z & 0 < r1;
f.x in rng f by A1,A4,FUNCT_1:3; then
reconsider y = f.x as Point of F;
diff(f,x) is invertible by A2,A4; then
consider r2 be Real such that
A5: 0 < r2 & Ball(y,r2) c= f.: Ball(x,r1) by A1,A4,Th18;
take y,r2;
thus thesis by A5;
end;
for y be Point of F st y in f.:Z
ex r be Real st 0 < r & Ball(y,r) c= f.:Z
proof
let y be Point of F;
assume y in f.:Z; then
consider x be object such that
A6: x in dom f & x in Z & y = f.x by FUNCT_1:def 6;
reconsider x as Point of E by A6;
consider r1 be Real such that
A7: 0 < r1 & Ball(x,r1) c= Z by A1,A6,NDIFF_8:20;
consider y1 be Point of F,r2 be Real such that
A8: y1 = f.x & 0 < r2 & Ball(y1,r2) c= f.: Ball(x,r1) by A3,A6,A7;
take r2;
thus 0 < r2 by A8;
f.: Ball(x,r1) c= f.:Z by A7,RELAT_1:123;
hence Ball(y,r2) c= f.:Z by A6,A8,XBOOLE_1:1;
end;
hence f.:Z is open by NDIFF_8:20;
end;