:: MFOLD_1 semantic presentation
begin
registration
let x, y be set ;
cluster{[x,y]} -> one-to-one ;
correctness
coherence
{[x,y]} is one-to-one ;
proof
set f = {[x,y]};
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom {[x,y]} or not x2 in dom {[x,y]} or not {[x,y]} . x1 = {[x,y]} . x2 or x1 = x2 )
assume ( x1 in dom {[x,y]} & x2 in dom {[x,y]} & {[x,y]} . x1 = {[x,y]} . x2 ) ; ::_thesis: x1 = x2
then A1: ( x1 in {x} & x2 in {x} ) by RELAT_1:9;
hence x1 = x by TARSKI:def_1
.= x2 by A1, TARSKI:def_1 ;
::_thesis: verum
end;
end;
theorem Th1: :: MFOLD_1:1
for T being non empty TopSpace holds T,T | ([#] T) are_homeomorphic
proof
let X be non empty TopSpace; ::_thesis: X,X | ([#] X) are_homeomorphic
set f = id X;
A1: dom (id X) = [#] X by RELAT_1:45;
A2: [#] (X | ([#] X)) = the carrier of TopStruct(# the carrier of X, the topology of X #) by TSEP_1:93
.= [#] X ;
then A3: rng (id X) = [#] (X | ([#] X)) by RELAT_1:45;
reconsider f = id X as Function of X,(X | ([#] X)) by A2;
for P being Subset of X st P is closed holds
(f ") " P is closed
proof
let P be Subset of X; ::_thesis: ( P is closed implies (f ") " P is closed )
assume P is closed ; ::_thesis: (f ") " P is closed
then ([#] X) \ P is open by PRE_TOPC:def_3;
then A4: ([#] X) \ P in the topology of X by PRE_TOPC:def_2;
A5: for x being set holds
( x in (f ") " P iff x in P )
proof
let x be set ; ::_thesis: ( x in (f ") " P iff x in P )
hereby ::_thesis: ( x in P implies x in (f ") " P )
assume A6: x in (f ") " P ; ::_thesis: x in P
x in f .: P by A6, A3, TOPS_2:54;
then consider y being set such that
A7: ( [y,x] in f & y in P ) by RELAT_1:def_13;
thus x in P by A7, RELAT_1:def_10; ::_thesis: verum
end;
assume A8: x in P ; ::_thesis: x in (f ") " P
then [x,x] in id X by RELAT_1:def_10;
then x in f .: P by A8, RELAT_1:def_13;
hence x in (f ") " P by A3, TOPS_2:54; ::_thesis: verum
end;
A9: ([#] X) \ P = ([#] (X | ([#] X))) \ ((f ") " P) by A2, A5, TARSKI:1;
([#] X) \ P = (([#] X) /\ ([#] X)) \ P
.= (([#] X) \ P) /\ ([#] X) by XBOOLE_1:49 ;
then ([#] X) \ P in the topology of (X | ([#] X)) by A2, A4, PRE_TOPC:def_4;
then ([#] (X | ([#] X))) \ ((f ") " P) is open by A9, PRE_TOPC:def_2;
hence (f ") " P is closed by PRE_TOPC:def_3; ::_thesis: verum
end;
then A10: f " is continuous by PRE_TOPC:def_6;
f is continuous by JGRAPH_1:45;
then f is being_homeomorphism by A1, A3, A10, TOPS_2:def_5;
hence X,X | ([#] X) are_homeomorphic by T_0TOPSP:def_1; ::_thesis: verum
end;
theorem Th2: :: MFOLD_1:2
for n being Nat
for X being non empty SubSpace of TOP-REAL n
for f being Function of X,R^1 st f is continuous holds
ex g being Function of X,(TOP-REAL n) st
( ( for a being Point of X
for b being Point of (TOP-REAL n)
for r being real number st a = b & f . a = r holds
g . b = r * b ) & g is continuous )
proof
let n be Nat; ::_thesis: for X being non empty SubSpace of TOP-REAL n
for f being Function of X,R^1 st f is continuous holds
ex g being Function of X,(TOP-REAL n) st
( ( for a being Point of X
for b being Point of (TOP-REAL n)
for r being real number st a = b & f . a = r holds
g . b = r * b ) & g is continuous )
let X be non empty SubSpace of TOP-REAL n; ::_thesis: for f being Function of X,R^1 st f is continuous holds
ex g being Function of X,(TOP-REAL n) st
( ( for a being Point of X
for b being Point of (TOP-REAL n)
for r being real number st a = b & f . a = r holds
g . b = r * b ) & g is continuous )
let f be Function of X,R^1; ::_thesis: ( f is continuous implies ex g being Function of X,(TOP-REAL n) st
( ( for a being Point of X
for b being Point of (TOP-REAL n)
for r being real number st a = b & f . a = r holds
g . b = r * b ) & g is continuous ) )
assume A1: f is continuous ; ::_thesis: ex g being Function of X,(TOP-REAL n) st
( ( for a being Point of X
for b being Point of (TOP-REAL n)
for r being real number st a = b & f . a = r holds
g . b = r * b ) & g is continuous )
defpred S1[ set , set ] means for b being Point of (TOP-REAL n)
for r being real number st $1 = b & f . $1 = r holds
$2 = r * b;
A2: for x being Element of X ex y being Point of (TOP-REAL n) st S1[x,y]
proof
let x be Element of X; ::_thesis: ex y being Point of (TOP-REAL n) st S1[x,y]
reconsider r = f . x as Real by TOPMETR:17;
A3: x in the carrier of X ;
[#] X c= [#] (TOP-REAL n) by PRE_TOPC:def_4;
then reconsider p = x as Point of (TOP-REAL n) by A3;
set y = r * p;
take r * p ; ::_thesis: S1[x,r * p]
thus S1[x,r * p] ; ::_thesis: verum
end;
ex g being Function of the carrier of X, the carrier of (TOP-REAL n) st
for x being Element of X holds S1[x,g . x] from FUNCT_2:sch_3(A2);
then consider g being Function of X,(TOP-REAL n) such that
A4: for x being Element of X
for b being Point of (TOP-REAL n)
for r being real number st x = b & f . x = r holds
g . x = r * b ;
take g ; ::_thesis: ( ( for a being Point of X
for b being Point of (TOP-REAL n)
for r being real number st a = b & f . a = r holds
g . b = r * b ) & g is continuous )
for p being Point of X
for V being Subset of (TOP-REAL n) st g . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & g .: W c= V )
proof
let p be Point of X; ::_thesis: for V being Subset of (TOP-REAL n) st g . p in V & V is open holds
ex W being Subset of X st
( p in W & W is open & g .: W c= V )
let V be Subset of (TOP-REAL n); ::_thesis: ( g . p in V & V is open implies ex W being Subset of X st
( p in W & W is open & g .: W c= V ) )
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
reconsider gp = g . p as Point of (Euclid n) by TOPREAL3:8;
A5: p in the carrier of X ;
[#] X c= [#] (TOP-REAL n) by PRE_TOPC:def_4;
then reconsider pp = p as Point of (TOP-REAL n1) by A5;
reconsider fp = f . p as real number ;
assume ( g . p in V & V is open ) ; ::_thesis: ex W being Subset of X st
( p in W & W is open & g .: W c= V )
then g . p in Int V by TOPS_1:23;
then consider r0 being real number such that
A6: r0 > 0 and
A7: Ball (gp,r0) c= V by GOBOARD6:5;
percases ( fp = 0 or fp <> 0 ) ;
supposeA8: fp = 0 ; ::_thesis: ex W being Subset of X st
( p in W & W is open & g .: W c= V )
reconsider W2 = (Ball (pp,(r0 / 2))) /\ ([#] X) as Subset of X ;
Ball (pp,(r0 / 2)) in the topology of (TOP-REAL n1) by PRE_TOPC:def_2;
then W2 in the topology of X by PRE_TOPC:def_4;
then A9: W2 is open by PRE_TOPC:def_2;
p in Ball (pp,(r0 / 2)) by A6, JORDAN:16;
then A10: p in W2 by XBOOLE_0:def_4;
set WW2 = { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } ;
A11: |.pp.| in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } by A10;
for x being set st x in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } holds
x is real
proof
let x be set ; ::_thesis: ( x in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } implies x is real )
assume x in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } ; ::_thesis: x is real
then consider p2 being Point of (TOP-REAL n1) such that
A12: ( x = |.p2.| & p2 in W2 ) ;
thus x is real by A12; ::_thesis: verum
end;
then reconsider WW2 = { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } as non empty real-membered set by A11, MEMBERED:def_3;
for x being ext-real number st x in WW2 holds
x <= |.pp.| + (r0 / 2)
proof
let x be ext-real number ; ::_thesis: ( x in WW2 implies x <= |.pp.| + (r0 / 2) )
assume x in WW2 ; ::_thesis: x <= |.pp.| + (r0 / 2)
then consider p2 being Point of (TOP-REAL n1) such that
A13: ( x = |.p2.| & p2 in W2 ) ;
p2 in Ball (pp,(r0 / 2)) by A13, XBOOLE_0:def_4;
then A14: |.(p2 - pp).| < r0 / 2 by TOPREAL9:7;
|.p2.| - |.(- pp).| <= |.(p2 + (- pp)).| by TOPRNS_1:31;
then |.p2.| - |.pp.| <= |.(p2 + (- pp)).| by TOPRNS_1:26;
then |.p2.| - |.pp.| <= r0 / 2 by A14, XXREAL_0:2;
then (|.p2.| - |.pp.|) + |.pp.| <= (r0 / 2) + |.pp.| by XREAL_1:6;
hence x <= |.pp.| + (r0 / 2) by A13; ::_thesis: verum
end;
then |.pp.| + (r0 / 2) is UpperBound of WW2 by XXREAL_2:def_1;
then WW2 is bounded_above by XXREAL_2:def_10;
then reconsider m = sup WW2 as real number ;
A15: m >= 0
proof
assume A16: m < 0 ; ::_thesis: contradiction
A17: m is UpperBound of WW2 by XXREAL_2:def_3;
|.pp.| in WW2 by A10;
hence contradiction by A16, A17, XXREAL_2:def_1; ::_thesis: verum
end;
percases ( m = 0 or m > 0 ) by A15;
supposeA18: m = 0 ; ::_thesis: ex W being Subset of X st
( p in W & W is open & g .: W c= V )
set G1 = REAL ;
REAL in the topology of R^1 by PRE_TOPC:def_1, TOPMETR:17;
then reconsider G1 = REAL as open Subset of R^1 by PRE_TOPC:def_2;
fp in G1 by XREAL_0:def_1;
then consider W1 being Subset of X such that
A19: p in W1 and
A20: W1 is open and
f .: W1 c= G1 by A1, JGRAPH_2:10;
reconsider W3 = W1 /\ W2 as Subset of X ;
take W3 ; ::_thesis: ( p in W3 & W3 is open & g .: W3 c= V )
thus p in W3 by A19, A10, XBOOLE_0:def_4; ::_thesis: ( W3 is open & g .: W3 c= V )
thus W3 is open by A20, A9; ::_thesis: g .: W3 c= V
g .: W3 c= Ball (gp,r0)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in g .: W3 or x in Ball (gp,r0) )
assume x in g .: W3 ; ::_thesis: x in Ball (gp,r0)
then consider q being set such that
A21: q in dom g and
A22: q in W3 and
A23: g . q = x by FUNCT_1:def_6;
reconsider q = q as Point of X by A21;
A24: q in the carrier of X ;
[#] X c= [#] (TOP-REAL n) by PRE_TOPC:def_4;
then reconsider qq = q as Point of (TOP-REAL n1) by A24;
reconsider fq = f . q as real number ;
A25: x = fq * qq by A4, A23;
then reconsider gq = x as Point of (Euclid n) by TOPREAL3:8;
reconsider gpp = gp as Point of (TOP-REAL n1) ;
reconsider gqq = gq as Point of (TOP-REAL n1) by A25;
A26: gpp = fp * pp by A4;
reconsider r2 = fq - fp as Real by XREAL_0:def_1;
A27: (abs (fq - fp)) * |.qq.| = (abs r2) * |.qq.|
.= |.((fq - fp) * qq).| by TOPRNS_1:7 ;
qq in W2 by A22, XBOOLE_0:def_4;
then |.qq.| in WW2 ;
then A28: |.qq.| <= m by XXREAL_2:4;
A29: gpp = 0. (TOP-REAL n1) by A26, A8, EUCLID:29;
|.(gqq + (- gpp)).| <= |.gqq.| + |.(- gpp).| by EUCLID_2:52;
then |.(gqq + (- gpp)).| <= |.gqq.| + |.(0. (TOP-REAL n1)).| by A29, JGRAPH_5:10;
then |.(gqq + (- gpp)).| <= |.gqq.| + 0 by EUCLID_2:39;
then |.(gqq - gpp).| < r0 by A4, A23, A8, A28, A27, A6, A18;
then gqq in Ball (gpp,r0) ;
hence x in Ball (gp,r0) by TOPREAL9:13; ::_thesis: verum
end;
hence g .: W3 c= V by A7, XBOOLE_1:1; ::_thesis: verum
end;
supposeA30: m > 0 ; ::_thesis: ex W being Subset of X st
( p in W & W is open & g .: W c= V )
set G1 = ].(fp - (r0 / m)),(fp + (r0 / m)).[;
reconsider G1 = ].(fp - (r0 / m)),(fp + (r0 / m)).[ as open Subset of R^1 by JORDAN6:35, TOPMETR:17, XXREAL_1:225;
A31: 0 + fp < (r0 / m) + fp by A30, A6, XREAL_1:6;
(- (r0 / m)) + fp < 0 + fp by A30, A6, XREAL_1:6;
then fp in G1 by A31, XXREAL_1:4;
then consider W1 being Subset of X such that
A32: p in W1 and
A33: W1 is open and
A34: f .: W1 c= G1 by A1, JGRAPH_2:10;
reconsider W3 = W1 /\ W2 as Subset of X ;
take W3 ; ::_thesis: ( p in W3 & W3 is open & g .: W3 c= V )
thus p in W3 by A32, A10, XBOOLE_0:def_4; ::_thesis: ( W3 is open & g .: W3 c= V )
thus W3 is open by A33, A9; ::_thesis: g .: W3 c= V
g .: W3 c= Ball (gp,r0)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in g .: W3 or x in Ball (gp,r0) )
assume x in g .: W3 ; ::_thesis: x in Ball (gp,r0)
then consider q being set such that
A35: q in dom g and
A36: q in W3 and
A37: g . q = x by FUNCT_1:def_6;
reconsider q = q as Point of X by A35;
A38: q in the carrier of X ;
[#] X c= [#] (TOP-REAL n) by PRE_TOPC:def_4;
then reconsider qq = q as Point of (TOP-REAL n1) by A38;
reconsider fq = f . q as real number ;
A39: x = fq * qq by A4, A37;
then reconsider gq = x as Point of (Euclid n) by TOPREAL3:8;
reconsider gpp = gp as Point of (TOP-REAL n1) ;
reconsider gqq = gq as Point of (TOP-REAL n1) by A39;
A40: gpp = fp * pp by A4;
reconsider r2 = fq as Real by XREAL_0:def_1;
A41: (abs fq) * |.qq.| = (abs r2) * |.qq.|
.= |.(fq * qq).| by TOPRNS_1:7 ;
A42: q in dom f by A38, FUNCT_2:def_1;
q in W1 by A36, XBOOLE_0:def_4;
then f . q in f .: W1 by A42, FUNCT_1:def_6;
then abs (fq - fp) < r0 / m by A34, RCOMP_1:1;
then (abs fq) * m < (r0 / m) * m by A8, A30, XREAL_1:68;
then (abs fq) * m < r0 / (m / m) by XCMPLX_1:82;
then A43: (abs fq) * m < r0 / 1 by A30, XCMPLX_1:60;
qq in W2 by A36, XBOOLE_0:def_4;
then |.qq.| in WW2 ;
then |.qq.| <= m by XXREAL_2:4;
then A44: |.qq.| * (abs fq) <= m * (abs fq) by XREAL_1:64;
A45: gpp = 0. (TOP-REAL n1) by A40, A8, EUCLID:29;
A46: |.gqq.| < r0 by A39, A44, A41, A43, XXREAL_0:2;
|.(gqq + (- gpp)).| <= |.gqq.| + |.(- gpp).| by EUCLID_2:52;
then |.(gqq + (- gpp)).| <= |.gqq.| + |.(0. (TOP-REAL n1)).| by A45, JGRAPH_5:10;
then |.(gqq + (- gpp)).| <= |.gqq.| + 0 by EUCLID_2:39;
then |.(gqq - gpp).| < r0 by A46, XXREAL_0:2;
then gqq in Ball (gpp,r0) ;
hence x in Ball (gp,r0) by TOPREAL9:13; ::_thesis: verum
end;
hence g .: W3 c= V by A7, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;
supposeA47: fp <> 0 ; ::_thesis: ex W being Subset of X st
( p in W & W is open & g .: W c= V )
reconsider W2 = (Ball (pp,((r0 / 2) / (abs fp)))) /\ ([#] X) as Subset of X ;
Ball (pp,((r0 / 2) / (abs fp))) in the topology of (TOP-REAL n1) by PRE_TOPC:def_2;
then W2 in the topology of X by PRE_TOPC:def_4;
then A48: W2 is open by PRE_TOPC:def_2;
p in Ball (pp,((r0 / 2) / (abs fp))) by A47, A6, JORDAN:16;
then A49: p in W2 by XBOOLE_0:def_4;
set WW2 = { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } ;
A50: |.pp.| in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } by A49;
for x being set st x in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } holds
x is real
proof
let x be set ; ::_thesis: ( x in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } implies x is real )
assume x in { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } ; ::_thesis: x is real
then consider p2 being Point of (TOP-REAL n1) such that
A51: ( x = |.p2.| & p2 in W2 ) ;
thus x is real by A51; ::_thesis: verum
end;
then reconsider WW2 = { |.p2.| where p2 is Point of (TOP-REAL n) : p2 in W2 } as non empty real-membered set by A50, MEMBERED:def_3;
for x being ext-real number st x in WW2 holds
x <= |.pp.| + ((r0 / 2) / (abs fp))
proof
let x be ext-real number ; ::_thesis: ( x in WW2 implies x <= |.pp.| + ((r0 / 2) / (abs fp)) )
assume x in WW2 ; ::_thesis: x <= |.pp.| + ((r0 / 2) / (abs fp))
then consider p2 being Point of (TOP-REAL n1) such that
A52: ( x = |.p2.| & p2 in W2 ) ;
p2 in Ball (pp,((r0 / 2) / (abs fp))) by A52, XBOOLE_0:def_4;
then A53: |.(p2 - pp).| < (r0 / 2) / (abs fp) by TOPREAL9:7;
|.p2.| - |.(- pp).| <= |.(p2 + (- pp)).| by TOPRNS_1:31;
then |.p2.| - |.pp.| <= |.(p2 + (- pp)).| by TOPRNS_1:26;
then |.p2.| - |.pp.| <= (r0 / 2) / (abs fp) by A53, XXREAL_0:2;
then (|.p2.| - |.pp.|) + |.pp.| <= ((r0 / 2) / (abs fp)) + |.pp.| by XREAL_1:6;
hence x <= |.pp.| + ((r0 / 2) / (abs fp)) by A52; ::_thesis: verum
end;
then |.pp.| + ((r0 / 2) / (abs fp)) is UpperBound of WW2 by XXREAL_2:def_1;
then WW2 is bounded_above by XXREAL_2:def_10;
then reconsider m = sup WW2 as real number ;
A54: m >= 0
proof
assume A55: m < 0 ; ::_thesis: contradiction
A56: m is UpperBound of WW2 by XXREAL_2:def_3;
|.pp.| in WW2 by A49;
hence contradiction by A55, A56, XXREAL_2:def_1; ::_thesis: verum
end;
percases ( m = 0 or m > 0 ) by A54;
supposeA57: m = 0 ; ::_thesis: ex W being Subset of X st
( p in W & W is open & g .: W c= V )
set G1 = REAL ;
REAL in the topology of R^1 by PRE_TOPC:def_1, TOPMETR:17;
then reconsider G1 = REAL as open Subset of R^1 by PRE_TOPC:def_2;
fp in G1 by XREAL_0:def_1;
then consider W1 being Subset of X such that
A58: p in W1 and
A59: W1 is open and
f .: W1 c= G1 by A1, JGRAPH_2:10;
reconsider W3 = W1 /\ W2 as Subset of X ;
take W3 ; ::_thesis: ( p in W3 & W3 is open & g .: W3 c= V )
thus p in W3 by A58, A49, XBOOLE_0:def_4; ::_thesis: ( W3 is open & g .: W3 c= V )
thus W3 is open by A59, A48; ::_thesis: g .: W3 c= V
g .: W3 c= Ball (gp,r0)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in g .: W3 or x in Ball (gp,r0) )
assume x in g .: W3 ; ::_thesis: x in Ball (gp,r0)
then consider q being set such that
A60: q in dom g and
A61: q in W3 and
A62: g . q = x by FUNCT_1:def_6;
reconsider q = q as Point of X by A60;
A63: q in the carrier of X ;
[#] X c= [#] (TOP-REAL n) by PRE_TOPC:def_4;
then reconsider qq = q as Point of (TOP-REAL n1) by A63;
reconsider fq = f . q as real number ;
A64: x = fq * qq by A4, A62;
then reconsider gq = x as Point of (Euclid n) by TOPREAL3:8;
reconsider gpp = gp as Point of (TOP-REAL n1) ;
reconsider gqq = gq as Point of (TOP-REAL n1) by A64;
A65: gpp = fp * pp by A4;
reconsider r2 = fq - fp as Real by XREAL_0:def_1;
reconsider r3 = fp as Real by XREAL_0:def_1;
A66: (abs (fq - fp)) * |.qq.| = (abs r2) * |.qq.|
.= |.((fq - fp) * qq).| by TOPRNS_1:7 ;
qq in W2 by A61, XBOOLE_0:def_4;
then |.qq.| in WW2 ;
then A67: |.qq.| <= m by XXREAL_2:4;
A68: (abs fp) * |.(qq - pp).| = (abs r3) * |.(qq - pp).|
.= |.(fp * (qq - pp)).| by TOPRNS_1:7 ;
qq in W2 by A61, XBOOLE_0:def_4;
then qq in Ball (pp,((r0 / 2) / (abs fp))) by XBOOLE_0:def_4;
then |.(qq - pp).| < (r0 / 2) / (abs fp) by TOPREAL9:7;
then (abs fp) * |.(qq - pp).| < (abs fp) * ((r0 / 2) / (abs fp)) by A47, XREAL_1:68;
then (abs fp) * |.(qq - pp).| < (r0 / 2) / ((abs fp) / (abs fp)) by XCMPLX_1:81;
then A69: (abs fp) * |.(qq - pp).| < (r0 / 2) / 1 by A47, XCMPLX_1:60;
A70: |.((fq - fp) * qq).| + |.(fp * (qq - pp)).| < (r0 / 2) + (r0 / 2) by A67, A69, A68, A66, A57, XREAL_1:8;
|.(((fq - fp) * qq) + (fp * (qq - pp))).| <= |.((fq - fp) * qq).| + |.(fp * (qq - pp)).| by EUCLID_2:52;
then A71: |.(((fq - fp) * qq) + (fp * (qq - pp))).| < r0 by A70, XXREAL_0:2;
((fq - fp) * qq) + (fp * (qq - pp)) = ((fq * qq) - (fp * qq)) + (fp * (qq - pp)) by EUCLID:50
.= ((fq * qq) - (fp * qq)) + ((fp * qq) - (fp * pp)) by EUCLID:49
.= (((fq * qq) - (fp * qq)) + (fp * qq)) - (fp * pp) by EUCLID:45
.= (fq * qq) - (fp * pp) by EUCLID:48 ;
then gqq in Ball (gpp,r0) by A64, A71, A65;
hence x in Ball (gp,r0) by TOPREAL9:13; ::_thesis: verum
end;
hence g .: W3 c= V by A7, XBOOLE_1:1; ::_thesis: verum
end;
supposeA72: m > 0 ; ::_thesis: ex W being Subset of X st
( p in W & W is open & g .: W c= V )
set G1 = ].(fp - ((r0 / 2) / m)),(fp + ((r0 / 2) / m)).[;
reconsider G1 = ].(fp - ((r0 / 2) / m)),(fp + ((r0 / 2) / m)).[ as open Subset of R^1 by JORDAN6:35, TOPMETR:17, XXREAL_1:225;
A73: 0 + fp < ((r0 / 2) / m) + fp by A72, A6, XREAL_1:6;
(- ((r0 / 2) / m)) + fp < 0 + fp by A72, A6, XREAL_1:6;
then fp in G1 by A73, XXREAL_1:4;
then consider W1 being Subset of X such that
A74: p in W1 and
A75: W1 is open and
A76: f .: W1 c= G1 by A1, JGRAPH_2:10;
reconsider W3 = W1 /\ W2 as Subset of X ;
take W3 ; ::_thesis: ( p in W3 & W3 is open & g .: W3 c= V )
thus p in W3 by A74, A49, XBOOLE_0:def_4; ::_thesis: ( W3 is open & g .: W3 c= V )
thus W3 is open by A75, A48; ::_thesis: g .: W3 c= V
g .: W3 c= Ball (gp,r0)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in g .: W3 or x in Ball (gp,r0) )
assume x in g .: W3 ; ::_thesis: x in Ball (gp,r0)
then consider q being set such that
A77: q in dom g and
A78: q in W3 and
A79: g . q = x by FUNCT_1:def_6;
reconsider q = q as Point of X by A77;
A80: q in the carrier of X ;
[#] X c= [#] (TOP-REAL n) by PRE_TOPC:def_4;
then reconsider qq = q as Point of (TOP-REAL n1) by A80;
reconsider fq = f . q as real number ;
A81: x = fq * qq by A4, A79;
then reconsider gq = x as Point of (Euclid n) by TOPREAL3:8;
reconsider gpp = gp as Point of (TOP-REAL n1) ;
reconsider gqq = gq as Point of (TOP-REAL n1) by A81;
A82: gpp = fp * pp by A4;
reconsider r2 = fq - fp as Real by XREAL_0:def_1;
reconsider r3 = fp as Real by XREAL_0:def_1;
A83: (abs (fq - fp)) * |.qq.| = (abs r2) * |.qq.|
.= |.((fq - fp) * qq).| by TOPRNS_1:7 ;
A84: q in dom f by A80, FUNCT_2:def_1;
q in W1 by A78, XBOOLE_0:def_4;
then f . q in f .: W1 by A84, FUNCT_1:def_6;
then abs (fq - fp) < (r0 / 2) / m by A76, RCOMP_1:1;
then (abs (fq - fp)) * m < ((r0 / 2) / m) * m by A72, XREAL_1:68;
then (abs (fq - fp)) * m < (r0 / 2) / (m / m) by XCMPLX_1:82;
then A85: (abs (fq - fp)) * m < (r0 / 2) / 1 by A72, XCMPLX_1:60;
qq in W2 by A78, XBOOLE_0:def_4;
then |.qq.| in WW2 ;
then |.qq.| <= m by XXREAL_2:4;
then |.qq.| * (abs (fq - fp)) <= m * (abs (fq - fp)) by XREAL_1:64;
then A86: |.((fq - fp) * qq).| < r0 / 2 by A83, A85, XXREAL_0:2;
A87: (abs fp) * |.(qq - pp).| = (abs r3) * |.(qq - pp).|
.= |.(fp * (qq - pp)).| by TOPRNS_1:7 ;
qq in W2 by A78, XBOOLE_0:def_4;
then qq in Ball (pp,((r0 / 2) / (abs fp))) by XBOOLE_0:def_4;
then |.(qq - pp).| < (r0 / 2) / (abs fp) by TOPREAL9:7;
then (abs fp) * |.(qq - pp).| < (abs fp) * ((r0 / 2) / (abs fp)) by A47, XREAL_1:68;
then (abs fp) * |.(qq - pp).| < (r0 / 2) / ((abs fp) / (abs fp)) by XCMPLX_1:81;
then A88: (abs fp) * |.(qq - pp).| < (r0 / 2) / 1 by A47, XCMPLX_1:60;
A89: |.((fq - fp) * qq).| + |.(fp * (qq - pp)).| < (r0 / 2) + (r0 / 2) by A86, A88, A87, XREAL_1:8;
|.(((fq - fp) * qq) + (fp * (qq - pp))).| <= |.((fq - fp) * qq).| + |.(fp * (qq - pp)).| by EUCLID_2:52;
then A90: |.(((fq - fp) * qq) + (fp * (qq - pp))).| < r0 by A89, XXREAL_0:2;
((fq - fp) * qq) + (fp * (qq - pp)) = ((fq * qq) - (fp * qq)) + (fp * (qq - pp)) by EUCLID:50
.= ((fq * qq) - (fp * qq)) + ((fp * qq) - (fp * pp)) by EUCLID:49
.= (((fq * qq) - (fp * qq)) + (fp * qq)) - (fp * pp) by EUCLID:45
.= (fq * qq) - (fp * pp) by EUCLID:48 ;
then gqq in Ball (gpp,r0) by A81, A82, A90;
hence x in Ball (gp,r0) by TOPREAL9:13; ::_thesis: verum
end;
hence g .: W3 c= V by A7, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;
end;
end;
hence ( ( for a being Point of X
for b being Point of (TOP-REAL n)
for r being real number st a = b & f . a = r holds
g . b = r * b ) & g is continuous ) by A4, JGRAPH_2:10; ::_thesis: verum
end;
definition
let n be Nat;
let S be Subset of (TOP-REAL n);
attrS is ball means :Def1: :: MFOLD_1:def 1
ex p being Point of (TOP-REAL n) ex r being real number st S = Ball (p,r);
end;
:: deftheorem Def1 defines ball MFOLD_1:def_1_:_
for n being Nat
for S being Subset of (TOP-REAL n) holds
( S is ball iff ex p being Point of (TOP-REAL n) ex r being real number st S = Ball (p,r) );
registration
let n be Nat;
cluster functional ball for Element of bool the carrier of (TOP-REAL n);
correctness
existence
ex b1 being Subset of (TOP-REAL n) st b1 is ball ;
proof
take Ball ( the Point of (TOP-REAL n), the real number ) ; ::_thesis: Ball ( the Point of (TOP-REAL n), the real number ) is ball
thus Ball ( the Point of (TOP-REAL n), the real number ) is ball by Def1; ::_thesis: verum
end;
cluster ball -> open for Element of bool the carrier of (TOP-REAL n);
correctness
coherence
for b1 being Subset of (TOP-REAL n) st b1 is ball holds
b1 is open ;
proof
let S be Subset of (TOP-REAL n); ::_thesis: ( S is ball implies S is open )
assume S is ball ; ::_thesis: S is open
then ex p being Point of (TOP-REAL n) ex r being real number st S = Ball (p,r) by Def1;
hence S is open ; ::_thesis: verum
end;
end;
registration
let n be Nat;
cluster non empty functional ball for Element of bool the carrier of (TOP-REAL n);
correctness
existence
ex b1 being Subset of (TOP-REAL n) st
( not b1 is empty & b1 is ball );
proof
reconsider S = Ball ((0. (TOP-REAL n)),1) as ball Subset of (TOP-REAL n) by Def1;
take S ; ::_thesis: ( not S is empty & S is ball )
thus ( not S is empty & S is ball ) ; ::_thesis: verum
end;
end;
theorem Th3: :: MFOLD_1:3
for n being Nat
for p being Point of (TOP-REAL n)
for S being open Subset of (TOP-REAL n) st p in S holds
ex B being ball Subset of (TOP-REAL n) st
( B c= S & p in B )
proof
let n be Nat; ::_thesis: for p being Point of (TOP-REAL n)
for S being open Subset of (TOP-REAL n) st p in S holds
ex B being ball Subset of (TOP-REAL n) st
( B c= S & p in B )
let p be Point of (TOP-REAL n); ::_thesis: for S being open Subset of (TOP-REAL n) st p in S holds
ex B being ball Subset of (TOP-REAL n) st
( B c= S & p in B )
let S be open Subset of (TOP-REAL n); ::_thesis: ( p in S implies ex B being ball Subset of (TOP-REAL n) st
( B c= S & p in B ) )
assume A1: p in S ; ::_thesis: ex B being ball Subset of (TOP-REAL n) st
( B c= S & p in B )
A2: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
A3: S in Family_open_set (Euclid n) by A2, PRE_TOPC:def_2;
reconsider x = p as Element of (Euclid n) by A2;
consider r being Real such that
A4: ( r > 0 & Ball (x,r) c= S ) by A1, A3, PCOMPS_1:def_4;
reconsider r = r as real positive number by A4;
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
reconsider B = Ball (p,r) as ball Subset of (TOP-REAL n) by Def1;
take B ; ::_thesis: ( B c= S & p in B )
reconsider p1 = p as Point of (TOP-REAL n1) ;
Ball (x,r) = Ball (p1,r) by TOPREAL9:13;
hence ( B c= S & p in B ) by A4, GOBOARD6:1; ::_thesis: verum
end;
definition
let n be Nat;
let p be Point of (TOP-REAL n);
let r be real number ;
func Tball (p,r) -> SubSpace of TOP-REAL n equals :: MFOLD_1:def 2
(TOP-REAL n) | (Ball (p,r));
correctness
coherence
(TOP-REAL n) | (Ball (p,r)) is SubSpace of TOP-REAL n;
;
end;
:: deftheorem defines Tball MFOLD_1:def_2_:_
for n being Nat
for p being Point of (TOP-REAL n)
for r being real number holds Tball (p,r) = (TOP-REAL n) | (Ball (p,r));
definition
let n be Nat;
func Tunit_ball n -> SubSpace of TOP-REAL n equals :: MFOLD_1:def 3
Tball ((0. (TOP-REAL n)),1);
correctness
coherence
Tball ((0. (TOP-REAL n)),1) is SubSpace of TOP-REAL n;
;
end;
:: deftheorem defines Tunit_ball MFOLD_1:def_3_:_
for n being Nat holds Tunit_ball n = Tball ((0. (TOP-REAL n)),1);
registration
let n be Nat;
cluster Tunit_ball n -> non empty ;
correctness
coherence
not Tunit_ball n is empty ;
;
let p be Point of (TOP-REAL n);
let s be real positive number ;
cluster Tball (p,s) -> non empty ;
correctness
coherence
not Tball (p,s) is empty ;
;
end;
theorem Th4: :: MFOLD_1:4
for n being Nat
for p being Point of (TOP-REAL n)
for r being real number holds the carrier of (Tball (p,r)) = Ball (p,r)
proof
let n be Nat; ::_thesis: for p being Point of (TOP-REAL n)
for r being real number holds the carrier of (Tball (p,r)) = Ball (p,r)
let p be Point of (TOP-REAL n); ::_thesis: for r being real number holds the carrier of (Tball (p,r)) = Ball (p,r)
let r be real number ; ::_thesis: the carrier of (Tball (p,r)) = Ball (p,r)
[#] (Tball (p,r)) = Ball (p,r) by PRE_TOPC:def_5;
hence the carrier of (Tball (p,r)) = Ball (p,r) ; ::_thesis: verum
end;
theorem Th5: :: MFOLD_1:5
for n being Nat
for p being Point of (TOP-REAL n) st n <> 0 & p is Point of (Tunit_ball n) holds
|.p.| < 1
proof
let n be Nat; ::_thesis: for p being Point of (TOP-REAL n) st n <> 0 & p is Point of (Tunit_ball n) holds
|.p.| < 1
let p be Point of (TOP-REAL n); ::_thesis: ( n <> 0 & p is Point of (Tunit_ball n) implies |.p.| < 1 )
reconsider j = 1 as real number ;
assume n <> 0 ; ::_thesis: ( not p is Point of (Tunit_ball n) or |.p.| < 1 )
then reconsider n1 = n as non empty Element of NAT by ORDINAL1:def_12;
assume p is Point of (Tunit_ball n) ; ::_thesis: |.p.| < 1
then p in the carrier of (Tball ((0. (TOP-REAL n1)),j)) ;
then p in Ball ((0. (TOP-REAL n1)),1) by Th4;
hence |.p.| < 1 by TOPREAL9:10; ::_thesis: verum
end;
theorem Th6: :: MFOLD_1:6
for n being Nat
for f being Function of (Tunit_ball n),(TOP-REAL n) st n <> 0 & ( for a being Point of (Tunit_ball n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (1 / (1 - (|.b.| * |.b.|))) * b ) holds
f is being_homeomorphism
proof
let n be Nat; ::_thesis: for f being Function of (Tunit_ball n),(TOP-REAL n) st n <> 0 & ( for a being Point of (Tunit_ball n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (1 / (1 - (|.b.| * |.b.|))) * b ) holds
f is being_homeomorphism
let f be Function of (Tunit_ball n),(TOP-REAL n); ::_thesis: ( n <> 0 & ( for a being Point of (Tunit_ball n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (1 / (1 - (|.b.| * |.b.|))) * b ) implies f is being_homeomorphism )
assume that
A1: n <> 0 and
A2: for a being Point of (Tunit_ball n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (1 / (1 - (|.b.| * |.b.|))) * b ; ::_thesis: f is being_homeomorphism
A3: dom f = [#] (Tunit_ball n) by FUNCT_2:def_1;
A4: [#] (Tunit_ball n) c= [#] (TOP-REAL n) by PRE_TOPC:def_4;
reconsider n1 = n as non empty Element of NAT by A1, ORDINAL1:def_12;
for y being set st y in [#] (TOP-REAL n1) holds
ex x being set st [x,y] in f
proof
let y be set ; ::_thesis: ( y in [#] (TOP-REAL n1) implies ex x being set st [x,y] in f )
assume y in [#] (TOP-REAL n1) ; ::_thesis: ex x being set st [x,y] in f
then reconsider py = y as Point of (TOP-REAL n1) ;
percases ( |.py.| = 0 or |.py.| <> 0 ) ;
supposeA5: |.py.| = 0 ; ::_thesis: ex x being set st [x,y] in f
set x = py;
|.(py - (0. (TOP-REAL n1))).| < 1 by A5, RLVECT_1:13;
then py in Ball ((0. (TOP-REAL n)),1) ;
then A6: py in dom f by A3, Th4;
take py ; ::_thesis: [py,y] in f
f . py = (1 / (1 - (|.py.| * |.py.|))) * py by A6, A2
.= py by A5, EUCLID:29 ;
hence [py,y] in f by A6, FUNCT_1:def_2; ::_thesis: verum
end;
supposeA7: |.py.| <> 0 ; ::_thesis: ex x being set st [x,y] in f
set p2 = |.py.| * |.py.|;
set x = (2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py;
reconsider r = 2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) as Real ;
A8: sqrt (1 + (4 * (|.py.| * |.py.|))) >= 0 by SQUARE_1:def_2;
A9: |.((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py).| = (abs r) * |.py.| by TOPRNS_1:7
.= r * |.py.| by A8, ABSVALUE:def_1 ;
|.((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py).| < 1
proof
(|.py.| * 4) + (1 + (4 * (|.py.| * |.py.|))) > 0 + (1 + (4 * (|.py.| * |.py.|))) by A7, XREAL_1:6;
then sqrt ((1 + (2 * |.py.|)) ^2) > sqrt (1 + (4 * (|.py.| * |.py.|))) by SQUARE_1:27;
then 1 + (2 * |.py.|) > sqrt (1 + (4 * (|.py.| * |.py.|))) by SQUARE_1:22;
then (1 + (2 * |.py.|)) - (sqrt (1 + (4 * (|.py.| * |.py.|)))) > (sqrt (1 + (4 * (|.py.| * |.py.|)))) - (sqrt (1 + (4 * (|.py.| * |.py.|)))) by XREAL_1:9;
then ((1 - (sqrt (1 + (4 * (|.py.| * |.py.|))))) + (2 * |.py.|)) - (2 * |.py.|) > 0 - (2 * |.py.|) by XREAL_1:9;
then (1 - (sqrt (1 + (4 * (|.py.| * |.py.|))))) * 1 > - (2 * |.py.|) ;
then (1 - (sqrt (1 + (4 * (|.py.| * |.py.|))))) * ((1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) > - (2 * |.py.|) by A8, XCMPLX_1:60;
then (1 - ((sqrt (1 + (4 * (|.py.| * |.py.|)))) ^2)) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) > - (2 * |.py.|) ;
then (1 - (1 + (4 * (|.py.| * |.py.|)))) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) > - (2 * |.py.|) by SQUARE_1:def_2;
then - ((4 * (|.py.| * |.py.|)) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) > - (2 * |.py.|) ;
then ((2 * |.py.|) * (2 * |.py.|)) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) < 2 * |.py.| by XREAL_1:24;
then ((2 * |.py.|) * ((2 * |.py.|) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))))) / (2 * |.py.|) < (2 * |.py.|) / (2 * |.py.|) by A7, XREAL_1:74;
then ((2 * |.py.|) * ((2 * |.py.|) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))))) / (2 * |.py.|) < 1 by A7, XCMPLX_1:60;
then ((2 * |.py.|) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) / ((2 * |.py.|) / (2 * |.py.|)) < 1 by XCMPLX_1:77;
then ((2 * |.py.|) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) / 1 < 1 by A7, XCMPLX_1:60;
hence |.((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py).| < 1 by A9; ::_thesis: verum
end;
then |.(((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py) - (0. (TOP-REAL n1))).| < 1 by RLVECT_1:13;
then (2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py in Ball ((0. (TOP-REAL n1)),1) ;
then A10: (2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py in dom f by A3, Th4;
take (2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py ; ::_thesis: [((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py),y] in f
A11: sqrt (1 + (4 * (|.py.| * |.py.|))) >= 0 by SQUARE_1:def_2;
A12: 1 - (sqrt (1 + (4 * (|.py.| * |.py.|)))) <> 0
proof
assume 1 - (sqrt (1 + (4 * (|.py.| * |.py.|)))) = 0 ; ::_thesis: contradiction
then (sqrt (1 + (4 * (|.py.| * |.py.|)))) ^2 = 1 ;
then 1 + (4 * (|.py.| * |.py.|)) = 1 by SQUARE_1:def_2;
hence contradiction by A7; ::_thesis: verum
end;
|.((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py).| * |.((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py).| = ((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * (2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))))) * (|.py.| * |.py.|) by A9
.= ((2 * 2) / ((1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) * (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))))) * (|.py.| * |.py.|) by XCMPLX_1:76
.= (4 / ((1 + (2 * (sqrt (1 + (4 * (|.py.| * |.py.|)))))) + ((sqrt (1 + (4 * (|.py.| * |.py.|)))) ^2))) * (|.py.| * |.py.|)
.= (4 / ((1 + (2 * (sqrt (1 + (4 * (|.py.| * |.py.|)))))) + (1 + (4 * (|.py.| * |.py.|))))) * (|.py.| * |.py.|) by SQUARE_1:def_2
.= (4 / (2 * ((1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) + (2 * (|.py.| * |.py.|))))) * (|.py.| * |.py.|)
.= ((4 / 2) / ((1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) + (2 * (|.py.| * |.py.|)))) * (|.py.| * |.py.|) by XCMPLX_1:78
.= (2 * (|.py.| * |.py.|)) / ((1 + (2 * (|.py.| * |.py.|))) + (sqrt (1 + (4 * (|.py.| * |.py.|))))) ;
then A13: 1 - (|.((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py).| * |.((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py).|) = (((1 + (2 * (|.py.| * |.py.|))) + (sqrt (1 + (4 * (|.py.| * |.py.|))))) / ((1 + (2 * (|.py.| * |.py.|))) + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) + (- ((2 * (|.py.| * |.py.|)) / ((1 + (2 * (|.py.| * |.py.|))) + (sqrt (1 + (4 * (|.py.| * |.py.|))))))) by A11, XCMPLX_1:60
.= ((1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) / ((1 + (2 * (|.py.| * |.py.|))) + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * 1
.= ((1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) / ((1 + (2 * (|.py.| * |.py.|))) + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * ((1 - (sqrt (1 + (4 * (|.py.| * |.py.|))))) / (1 - (sqrt (1 + (4 * (|.py.| * |.py.|)))))) by A12, XCMPLX_1:60
.= ((1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) * (1 - (sqrt (1 + (4 * (|.py.| * |.py.|)))))) / ((1 - (sqrt (1 + (4 * (|.py.| * |.py.|))))) * ((1 + (2 * (|.py.| * |.py.|))) + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) by XCMPLX_1:76
.= (1 - ((sqrt (1 + (4 * (|.py.| * |.py.|)))) ^2)) / (((1 + (2 * (|.py.| * |.py.|))) - ((2 * (|.py.| * |.py.|)) * (sqrt (1 + (4 * (|.py.| * |.py.|)))))) - ((sqrt (1 + (4 * (|.py.| * |.py.|)))) * (sqrt (1 + (4 * (|.py.| * |.py.|))))))
.= (1 - (1 + (4 * (|.py.| * |.py.|)))) / (((1 + (2 * (|.py.| * |.py.|))) - ((2 * (|.py.| * |.py.|)) * (sqrt (1 + (4 * (|.py.| * |.py.|)))))) - ((sqrt (1 + (4 * (|.py.| * |.py.|)))) ^2)) by SQUARE_1:def_2
.= (- (4 * (|.py.| * |.py.|))) / (((1 + (2 * (|.py.| * |.py.|))) - ((2 * (|.py.| * |.py.|)) * (sqrt (1 + (4 * (|.py.| * |.py.|)))))) - (1 + (4 * (|.py.| * |.py.|)))) by SQUARE_1:def_2
.= (- (4 * (|.py.| * |.py.|))) / ((- (2 * (|.py.| * |.py.|))) * (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))))
.= ((2 * (- (2 * (|.py.| * |.py.|)))) / (- (2 * (|.py.| * |.py.|)))) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) by XCMPLX_1:78
.= (2 * ((- (2 * (|.py.| * |.py.|))) / (- (2 * (|.py.| * |.py.|))))) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))
.= (2 * 1) / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) by A7, XCMPLX_1:60
.= 2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|))))) ;
f . ((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py) = (1 / (1 - (|.((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py).| * |.((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py).|))) * ((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py) by A2, A10
.= (r / r) * py by A13, EUCLID:30
.= 1 * py by A8, XCMPLX_1:60
.= py by EUCLID:29 ;
hence [((2 / (1 + (sqrt (1 + (4 * (|.py.| * |.py.|)))))) * py),y] in f by A10, FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
then A14: rng f = [#] (TOP-REAL n1) by RELSET_1:10;
for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
A15: [#] (Tunit_ball n) c= [#] (TOP-REAL n) by PRE_TOPC:def_4;
assume A16: x1 in dom f ; ::_thesis: ( not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
then x1 in the carrier of (Tunit_ball n) ;
then reconsider px1 = x1 as Point of (TOP-REAL n1) by A15;
assume A17: x2 in dom f ; ::_thesis: ( not f . x1 = f . x2 or x1 = x2 )
then A18: x2 in the carrier of (Tunit_ball n) ;
then reconsider px2 = x2 as Point of (TOP-REAL n1) by A15;
assume A19: f . x1 = f . x2 ; ::_thesis: x1 = x2
A20: (1 / (1 - (|.px1.| * |.px1.|))) * px1 = f . x2 by A19, A16, A2
.= (1 / (1 - (|.px2.| * |.px2.|))) * px2 by A17, A2 ;
percases ( |.px1.| = 0 or |.px1.| <> 0 ) ;
supposeA21: |.px1.| = 0 ; ::_thesis: x1 = x2
then A22: px1 = 0. (TOP-REAL n) by EUCLID_2:42;
percases ( 1 / (1 - (|.px2.| * |.px2.|)) = 0 or px2 = 0. (TOP-REAL n) ) by A22, A20, EUCLID:28, EUCLID:31;
suppose 1 / (1 - (|.px2.| * |.px2.|)) = 0 ; ::_thesis: x1 = x2
then 1 - (|.px2.| * |.px2.|) = 0 ;
then sqrt (|.px2.| ^2) = 1 by SQUARE_1:18;
then A23: |.px2.| = 1 by SQUARE_1:22;
px2 in Ball ((0. (TOP-REAL n)),1) by A18, Th4;
then consider p2 being Point of (TOP-REAL n) such that
A24: ( p2 = px2 & |.(p2 - (0. (TOP-REAL n))).| < 1 ) ;
thus x1 = x2 by A23, A24, RLVECT_1:13; ::_thesis: verum
end;
suppose px2 = 0. (TOP-REAL n) ; ::_thesis: x1 = x2
hence x1 = x2 by A21, EUCLID_2:42; ::_thesis: verum
end;
end;
end;
supposeA25: |.px1.| <> 0 ; ::_thesis: x1 = x2
then |.px1.| * |.px1.| < 1 * |.px1.| by A16, Th5, XREAL_1:68;
then |.px1.| * |.px1.| < 1 by A16, Th5, XXREAL_0:2;
then - (|.px1.| * |.px1.|) > - 1 by XREAL_1:24;
then A26: (- (|.px1.| * |.px1.|)) + 1 > (- 1) + 1 by XREAL_1:6;
A27: px1 = 1 * px1 by EUCLID:29
.= ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px1.| * |.px1.|))) * px1 by A26, XCMPLX_1:60
.= (1 - (|.px1.| * |.px1.|)) * ((1 / (1 - (|.px1.| * |.px1.|))) * px1) by EUCLID:30
.= ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * px2 by A20, EUCLID:30 ;
A28: px2 <> 0. (TOP-REAL n1)
proof
assume px2 = 0. (TOP-REAL n1) ; ::_thesis: contradiction
then px1 = 0. (TOP-REAL n1) by A27, EUCLID:28;
hence contradiction by A25, TOPRNS_1:23; ::_thesis: verum
end;
then A29: |.px2.| <> 0 by EUCLID_2:42;
px2 in Ball ((0. (TOP-REAL n)),1) by A18, Th4;
then consider p2 being Point of (TOP-REAL n) such that
A30: ( p2 = px2 & |.(p2 - (0. (TOP-REAL n))).| < 1 ) ;
A31: |.px2.| < 1 by A30, RLVECT_1:13;
then |.px2.| * |.px2.| < 1 * |.px2.| by A29, XREAL_1:68;
then |.px2.| * |.px2.| < 1 by A31, XXREAL_0:2;
then - (|.px2.| * |.px2.|) > - 1 by XREAL_1:24;
then A32: (- (|.px2.| * |.px2.|)) + 1 > (- 1) + 1 by XREAL_1:6;
set l = (1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|));
(1 / (1 - (|.px2.| * |.px2.|))) * px2 = ((1 / (1 - (|.px1.| * |.px1.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) * px2 by A27, A20, EUCLID:30;
then ((1 / (1 - (|.px2.| * |.px2.|))) * px2) - (((1 / (1 - (|.px1.| * |.px1.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) * px2) = 0. (TOP-REAL n) by EUCLID:36;
then ((1 / (1 - (|.px2.| * |.px2.|))) * px2) + ((- ((1 / (1 - (|.px1.| * |.px1.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))))) * px2) = 0. (TOP-REAL n) by EUCLID:40;
then A33: ((1 / (1 - (|.px2.| * |.px2.|))) + (- ((1 / (1 - (|.px1.| * |.px1.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))))) * px2 = 0. (TOP-REAL n) by EUCLID:33;
A34: ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) = (abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) * (abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))))
proof
percases ( abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) = (1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)) or abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) = - ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) ) by ABSVALUE:1;
suppose abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) = (1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)) ; ::_thesis: ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) = (abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) * (abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))))
hence ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) = (abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) * (abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) ; ::_thesis: verum
end;
suppose abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) = - ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) ; ::_thesis: ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) = (abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) * (abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))))
hence ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) = (abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) * (abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) ; ::_thesis: verum
end;
end;
end;
(1 / (1 - (|.px2.| * |.px2.|))) + (- ((1 / (1 - (|.px1.| * |.px1.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))))) = 0 by A28, A33, EUCLID:31;
then 1 / (1 - (|.px2.| * |.px2.|)) = (1 * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) / (1 - (|.px1.| * |.px1.|))
.= 1 / ((1 - (|.px1.| * |.px1.|)) / ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) by XCMPLX_1:77 ;
then 1 - (|.px2.| * |.px2.|) = (1 - (|.px1.| * |.px1.|)) / ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) by XCMPLX_1:59;
then ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * (1 - (|.px2.| * |.px2.|)) = (1 - (|.px1.| * |.px1.|)) / (((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) / ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) by XCMPLX_1:81
.= (1 - (|.px1.| * |.px1.|)) / 1 by A26, A32, XCMPLX_1:60
.= 1 - (((abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) * |.px2.|) * |.(((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * px2).|) by A27, TOPRNS_1:7
.= 1 - (((abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) * |.px2.|) * ((abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) * |.px2.|)) by TOPRNS_1:7
.= 1 - ((((abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) * (abs ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))))) * |.px2.|) * |.px2.|)
.= 1 - (((((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) * |.px2.|) * |.px2.|) by A34 ;
then (1 + ((((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) * |.px2.|) * |.px2.|)) * (1 - ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|)))) = 0 ;
then 1 - ((1 - (|.px1.| * |.px1.|)) / (1 - (|.px2.| * |.px2.|))) = 0 by A26, A32;
hence x1 = x2 by A27, EUCLID:29; ::_thesis: verum
end;
end;
end;
then A35: f is one-to-one by FUNCT_1:def_4;
consider f0 being Function of (TOP-REAL n1),R^1 such that
A36: ( ( for p being Point of (TOP-REAL n1) holds f0 . p = 1 ) & f0 is continuous ) by JGRAPH_2:20;
consider f1 being Function of (TOP-REAL n1),R^1 such that
A37: ( ( for p being Point of (TOP-REAL n1) holds f1 . p = |.p.| ) & f1 is continuous ) by JORDAN2C:84;
consider f2 being Function of (TOP-REAL n),R^1 such that
A38: ( ( for p being Point of (TOP-REAL n)
for r1 being real number st f1 . p = r1 holds
f2 . p = r1 * r1 ) & f2 is continuous ) by A37, JGRAPH_2:22;
consider f3 being Function of (TOP-REAL n),R^1 such that
A39: ( ( for p being Point of (TOP-REAL n)
for r1, r2 being real number st f0 . p = r1 & f2 . p = r2 holds
f3 . p = r1 - r2 ) & f3 is continuous ) by A36, A38, JGRAPH_2:21;
reconsider f3 = f3 as continuous Function of (TOP-REAL n),R^1 by A39;
A40: for p being Point of (TOP-REAL n) holds f3 . p = 1 - (|.p.| * |.p.|)
proof
let p be Point of (TOP-REAL n); ::_thesis: f3 . p = 1 - (|.p.| * |.p.|)
thus f3 . p = (f0 . p) - (f2 . p) by A39
.= 1 - (f2 . p) by A36
.= 1 - ((f1 . p) * (f1 . p)) by A38
.= 1 - (|.p.| * (f1 . p)) by A37
.= 1 - (|.p.| * |.p.|) by A37 ; ::_thesis: verum
end;
set f4 = f3 | (Tunit_ball n);
for p being Point of (Tunit_ball n) holds (f3 | (Tunit_ball n)) . p <> 0
proof
let p be Point of (Tunit_ball n); ::_thesis: (f3 | (Tunit_ball n)) . p <> 0
assume (f3 | (Tunit_ball n)) . p = 0 ; ::_thesis: contradiction
then A41: f3 . p = 0 by FUNCT_1:49;
p in the carrier of (Tunit_ball n) ;
then reconsider p1 = p as Point of (TOP-REAL n1) by A4;
A42: 1 - (|.p1.| * |.p1.|) = 0 by A41, A40;
percases ( |.p1.| = 0 or |.p1.| <> 0 ) ;
suppose |.p1.| = 0 ; ::_thesis: contradiction
hence contradiction by A42; ::_thesis: verum
end;
suppose |.p1.| <> 0 ; ::_thesis: contradiction
then |.p1.| * |.p1.| < 1 * |.p1.| by Th5, XREAL_1:68;
hence contradiction by A42, Th5; ::_thesis: verum
end;
end;
end;
then consider f5 being Function of (Tunit_ball n),R^1 such that
A43: ( ( for p being Point of (Tunit_ball n)
for r1 being real number st (f3 | (Tunit_ball n)) . p = r1 holds
f5 . p = 1 / r1 ) & f5 is continuous ) by JGRAPH_2:26;
consider f6 being Function of (Tunit_ball n),(TOP-REAL n) such that
A44: ( ( for a being Point of (Tunit_ball n)
for b being Point of (TOP-REAL n)
for r being real number st a = b & f5 . a = r holds
f6 . b = r * b ) & f6 is continuous ) by A43, Th2;
A45: dom f = the carrier of (Tunit_ball n) by FUNCT_2:def_1
.= dom f6 by FUNCT_2:def_1 ;
for x being set st x in dom f holds
f . x = f6 . x
proof
let x be set ; ::_thesis: ( x in dom f implies f . x = f6 . x )
assume A46: x in dom f ; ::_thesis: f . x = f6 . x
then A47: x in the carrier of (Tunit_ball n) ;
reconsider p1 = x as Point of (Tunit_ball n) by A46;
reconsider p = x as Point of (TOP-REAL n) by A47, A4;
(f3 | (Tunit_ball n)) . p = f3 . p by A46, FUNCT_1:49
.= 1 - (|.p.| * |.p.|) by A40 ;
then f5 . p1 = 1 / (1 - (|.p.| * |.p.|)) by A43;
then f6 . p1 = (1 / (1 - (|.p.| * |.p.|))) * p by A44;
hence f . x = f6 . x by A2; ::_thesis: verum
end;
then A48: f = f6 by A45, FUNCT_1:2;
consider f8 being Function of (TOP-REAL n),R^1 such that
A49: ( ( for p being Point of (TOP-REAL n)
for r1 being real number st f2 . p = r1 holds
f8 . p = 4 * r1 ) & f8 is continuous ) by A38, JGRAPH_2:23;
consider f9 being Function of (TOP-REAL n),R^1 such that
A50: ( ( for p being Point of (TOP-REAL n)
for r1, r2 being real number st f0 . p = r1 & f8 . p = r2 holds
f9 . p = r1 + r2 ) & f9 is continuous ) by A49, A36, JGRAPH_2:19;
A51: for p being Point of (TOP-REAL n) holds f9 . p = 1 + ((4 * |.p.|) * |.p.|)
proof
let p be Point of (TOP-REAL n); ::_thesis: f9 . p = 1 + ((4 * |.p.|) * |.p.|)
thus f9 . p = (f0 . p) + (f8 . p) by A50
.= 1 + (f8 . p) by A36
.= 1 + (4 * (f2 . p)) by A49
.= 1 + (4 * ((f1 . p) * (f1 . p))) by A38
.= 1 + (4 * ((f1 . p) * |.p.|)) by A37
.= 1 + (4 * (|.p.| * |.p.|)) by A37
.= 1 + ((4 * |.p.|) * |.p.|) ; ::_thesis: verum
end;
A52: for p being Point of (TOP-REAL n) ex r being real number st
( f9 . p = r & r >= 0 )
proof
let p be Point of (TOP-REAL n); ::_thesis: ex r being real number st
( f9 . p = r & r >= 0 )
set r = 1 + ((4 * |.p.|) * |.p.|);
take 1 + ((4 * |.p.|) * |.p.|) ; ::_thesis: ( f9 . p = 1 + ((4 * |.p.|) * |.p.|) & 1 + ((4 * |.p.|) * |.p.|) >= 0 )
thus ( f9 . p = 1 + ((4 * |.p.|) * |.p.|) & 1 + ((4 * |.p.|) * |.p.|) >= 0 ) by A51; ::_thesis: verum
end;
consider f10 being Function of (TOP-REAL n),R^1 such that
A53: ( ( for p being Point of (TOP-REAL n)
for r1 being real number st f9 . p = r1 holds
f10 . p = sqrt r1 ) & f10 is continuous ) by A52, A50, JGRAPH_3:5;
consider f11 being Function of (TOP-REAL n),R^1 such that
A54: ( ( for p being Point of (TOP-REAL n)
for r1, r2 being real number st f0 . p = r1 & f10 . p = r2 holds
f11 . p = r1 + r2 ) & f11 is continuous ) by A53, A36, JGRAPH_2:19;
for p being Point of (TOP-REAL n) holds f11 . p <> 0
proof
let p be Point of (TOP-REAL n); ::_thesis: f11 . p <> 0
A55: f11 . p = (f0 . p) + (f10 . p) by A54
.= 1 + (f10 . p) by A36
.= 1 + (sqrt (f9 . p)) by A53 ;
consider r being real number such that
A56: ( r = f9 . p & r >= 0 ) by A52;
sqrt (f9 . p) >= 0 by A56, SQUARE_1:def_2;
hence f11 . p <> 0 by A55; ::_thesis: verum
end;
then consider f12 being Function of (TOP-REAL n),R^1 such that
A57: ( ( for p being Point of (TOP-REAL n)
for r1 being real number st f11 . p = r1 holds
f12 . p = 1 / r1 ) & f12 is continuous ) by A54, JGRAPH_2:26;
consider f13 being Function of (TOP-REAL n),R^1 such that
A58: ( ( for p being Point of (TOP-REAL n)
for r1 being real number st f12 . p = r1 holds
f13 . p = 2 * r1 ) & f13 is continuous ) by A57, JGRAPH_2:23;
A59: for p being Point of (TOP-REAL n) holds f13 . p = 2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|))))
proof
let p be Point of (TOP-REAL n); ::_thesis: f13 . p = 2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|))))
thus f13 . p = 2 * (f12 . p) by A58
.= 2 * (1 / (f11 . p)) by A57
.= 2 / ((f0 . p) + (f10 . p)) by A54
.= 2 / ((f0 . p) + (sqrt (f9 . p))) by A53
.= 2 / (1 + (sqrt (f9 . p))) by A36
.= 2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) by A51 ; ::_thesis: verum
end;
reconsider X = TOP-REAL n as non empty SubSpace of TOP-REAL n by TSEP_1:2;
consider f14 being Function of X,(TOP-REAL n) such that
A60: ( ( for a being Point of X
for b being Point of (TOP-REAL n)
for r being real number st a = b & f13 . a = r holds
f14 . b = r * b ) & f14 is continuous ) by A58, Th2;
reconsider f14 = f14 as continuous Function of (TOP-REAL n),(TOP-REAL n) by A60;
A61: dom f14 = the carrier of (TOP-REAL n) by FUNCT_2:def_1;
A62: for r being real number holds (abs r) * (abs r) = r * r
proof
let r be real number ; ::_thesis: (abs r) * (abs r) = r * r
percases ( abs r = r or abs r = - r ) by ABSVALUE:1;
suppose abs r = r ; ::_thesis: (abs r) * (abs r) = r * r
hence (abs r) * (abs r) = r * r ; ::_thesis: verum
end;
suppose abs r = - r ; ::_thesis: (abs r) * (abs r) = r * r
hence (abs r) * (abs r) = r * r ; ::_thesis: verum
end;
end;
end;
for y being set holds
( y in the carrier of (Tunit_ball n) iff ex x being set st
( x in dom f14 & y = f14 . x ) )
proof
let y be set ; ::_thesis: ( y in the carrier of (Tunit_ball n) iff ex x being set st
( x in dom f14 & y = f14 . x ) )
hereby ::_thesis: ( ex x being set st
( x in dom f14 & y = f14 . x ) implies y in the carrier of (Tunit_ball n) )
assume A63: y in the carrier of (Tunit_ball n) ; ::_thesis: ex x being set st
( x in dom f14 & f14 . x = y )
[#] (Tunit_ball n) c= [#] (TOP-REAL n) by PRE_TOPC:def_4;
then reconsider q = y as Point of (TOP-REAL n1) by A63;
|.q.| < 1 by A63, Th5;
then |.q.| * |.q.| <= 1 * |.q.| by XREAL_1:64;
then |.q.| * |.q.| < 1 by A63, Th5, XXREAL_0:2;
then A64: 0 < 1 - (|.q.| * |.q.|) by XREAL_1:50;
set p = (1 / (1 - (|.q.| * |.q.|))) * q;
|.((1 / (1 - (|.q.| * |.q.|))) * q).| = (abs (1 / (1 - (|.q.| * |.q.|)))) * |.q.| by TOPRNS_1:7;
then |.((1 / (1 - (|.q.| * |.q.|))) * q).| * |.((1 / (1 - (|.q.| * |.q.|))) * q).| = (((abs (1 / (1 - (|.q.| * |.q.|)))) * (abs (1 / (1 - (|.q.| * |.q.|))))) * |.q.|) * |.q.|
.= (((1 / (1 - (|.q.| * |.q.|))) * (1 / (1 - (|.q.| * |.q.|)))) * |.q.|) * |.q.| by A62
.= (((1 * 1) / ((1 - (|.q.| * |.q.|)) * (1 - (|.q.| * |.q.|)))) * |.q.|) * |.q.| by XCMPLX_1:76
.= (|.q.| * |.q.|) / ((1 - (|.q.| * |.q.|)) * (1 - (|.q.| * |.q.|))) ;
then A65: 1 + ((4 * |.((1 / (1 - (|.q.| * |.q.|))) * q).|) * |.((1 / (1 - (|.q.| * |.q.|))) * q).|) = (((1 - (|.q.| * |.q.|)) * (1 - (|.q.| * |.q.|))) / ((1 - (|.q.| * |.q.|)) * (1 - (|.q.| * |.q.|)))) + (((4 * |.q.|) * |.q.|) / ((1 - (|.q.| * |.q.|)) * (1 - (|.q.| * |.q.|)))) by A64, XCMPLX_1:60
.= ((1 + (|.q.| * |.q.|)) * (1 + (|.q.| * |.q.|))) / ((1 - (|.q.| * |.q.|)) * (1 - (|.q.| * |.q.|)))
.= ((1 + (|.q.| * |.q.|)) / (1 - (|.q.| * |.q.|))) ^2 by XCMPLX_1:76 ;
sqrt (1 + ((4 * |.((1 / (1 - (|.q.| * |.q.|))) * q).|) * |.((1 / (1 - (|.q.| * |.q.|))) * q).|)) = (1 + (|.q.| * |.q.|)) / (1 - (|.q.| * |.q.|)) by A64, A65, SQUARE_1:22;
then A66: 1 + (sqrt (1 + ((4 * |.((1 / (1 - (|.q.| * |.q.|))) * q).|) * |.((1 / (1 - (|.q.| * |.q.|))) * q).|))) = ((1 - (|.q.| * |.q.|)) / (1 - (|.q.| * |.q.|))) + ((1 + (|.q.| * |.q.|)) / (1 - (|.q.| * |.q.|))) by A64, XCMPLX_1:60
.= 2 / (1 - (|.q.| * |.q.|)) ;
reconsider x = (1 / (1 - (|.q.| * |.q.|))) * q as set ;
take x = x; ::_thesis: ( x in dom f14 & f14 . x = y )
thus x in dom f14 by A61; ::_thesis: f14 . x = y
thus f14 . x = (f13 . ((1 / (1 - (|.q.| * |.q.|))) * q)) * ((1 / (1 - (|.q.| * |.q.|))) * q) by A60
.= (2 / (2 / (1 - (|.q.| * |.q.|)))) * ((1 / (1 - (|.q.| * |.q.|))) * q) by A66, A59
.= (1 - (|.q.| * |.q.|)) * ((1 / (1 - (|.q.| * |.q.|))) * q) by XCMPLX_1:52
.= ((1 - (|.q.| * |.q.|)) / (1 - (|.q.| * |.q.|))) * q by EUCLID:30
.= 1 * q by A64, XCMPLX_1:60
.= y by EUCLID:29 ; ::_thesis: verum
end;
given x being set such that A67: ( x in dom f14 & y = f14 . x ) ; ::_thesis: y in the carrier of (Tunit_ball n)
reconsider p = x as Point of (TOP-REAL n1) by A67;
y in rng f14 by A67, FUNCT_1:3;
then reconsider q = y as Point of (TOP-REAL n1) ;
y = (f13 . p) * p by A60, A67
.= (2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|))))) * p by A59 ;
then |.q.| = (abs (2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))))) * |.p.| by TOPRNS_1:7;
then A68: |.q.| * |.q.| = (((abs (2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))))) * (abs (2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|))))))) * |.p.|) * |.p.|
.= (((2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|))))) * (2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))))) * |.p.|) * |.p.| by A62 ;
|.q.| * |.q.| < 1
proof
assume |.q.| * |.q.| >= 1 ; ::_thesis: contradiction
then A69: (((2 * 2) / ((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) * (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))))) * |.p.|) * |.p.| >= 1 by A68, XCMPLX_1:76;
0 <= sqrt (1 + ((4 * |.p.|) * |.p.|)) by SQUARE_1:def_2;
then (((4 / ((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) ^2)) * |.p.|) * |.p.|) * ((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) ^2) >= 1 * ((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) ^2) by A69, XREAL_1:64;
then (((((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) ^2) / ((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) ^2)) * 4) * |.p.|) * |.p.| >= (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) ^2 ;
then ((1 * 4) * |.p.|) * |.p.| >= (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) ^2 by XCMPLX_1:60;
then (4 * |.p.|) * |.p.| >= (1 + (2 * (sqrt (1 + ((4 * |.p.|) * |.p.|))))) + ((sqrt (1 + ((4 * |.p.|) * |.p.|))) ^2) ;
then (4 * |.p.|) * |.p.| >= (1 + (2 * (sqrt (1 + ((4 * |.p.|) * |.p.|))))) + (1 + ((4 * |.p.|) * |.p.|)) by SQUARE_1:def_2;
then ((4 * |.p.|) * |.p.|) - ((4 * |.p.|) * |.p.|) >= ((2 + (2 * (sqrt (1 + ((4 * |.p.|) * |.p.|))))) + ((4 * |.p.|) * |.p.|)) - ((4 * |.p.|) * |.p.|) by XREAL_1:9;
then 0 / 2 > (2 * (sqrt (1 + ((4 * |.p.|) * |.p.|)))) / 2 ;
hence contradiction by SQUARE_1:def_2; ::_thesis: verum
end;
then |.q.| ^2 < 1 ;
then A70: |.q.| < 1 by SQUARE_1:52;
|.(q + (- (0. (TOP-REAL n1)))).| <= |.q.| + |.(- (0. (TOP-REAL n1))).| by EUCLID_2:52;
then |.(q + (- (0. (TOP-REAL n1)))).| <= |.q.| + |.(0. (TOP-REAL n1)).| by JGRAPH_5:10;
then |.(q + (- (0. (TOP-REAL n1)))).| <= |.q.| + 0 by EUCLID_2:39;
then |.(q - (0. (TOP-REAL n1))).| < 1 by A70, XXREAL_0:2;
then q in Ball ((0. (TOP-REAL n1)),1) ;
then y in [#] (Tball ((0. (TOP-REAL n)),1)) by PRE_TOPC:def_5;
hence y in the carrier of (Tunit_ball n) ; ::_thesis: verum
end;
then A71: rng f14 = the carrier of (Tunit_ball n) by FUNCT_1:def_3;
then reconsider f14 = f14 as Function of (TOP-REAL n),(Tunit_ball n) by A61, FUNCT_2:1;
A72: dom f14 = the carrier of (TOP-REAL n) by FUNCT_2:def_1
.= dom (f ") by FUNCT_2:def_1 ;
for x being set st x in dom f14 holds
f14 . x = (f ") . x
proof
let x be set ; ::_thesis: ( x in dom f14 implies f14 . x = (f ") . x )
assume A73: x in dom f14 ; ::_thesis: f14 . x = (f ") . x
reconsider g = f as Function ;
f is onto by A14, FUNCT_2:def_3;
then A74: f " = g " by A35, TOPS_2:def_4;
A75: f14 . x in rng f14 by A73, FUNCT_1:3;
then A76: f14 . x in dom f by A71, FUNCT_2:def_1;
reconsider p = x as Point of (TOP-REAL n1) by A73;
A77: f14 . p = (f13 . p) * p by A60
.= (2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|))))) * p by A59 ;
reconsider y = f14 . x as Point of (Tunit_ball n) by A75;
f14 . x in [#] (Tunit_ball n) by A75;
then reconsider q = y as Point of (TOP-REAL n1) by A4;
A78: 0 <= sqrt (1 + ((4 * |.p.|) * |.p.|)) by SQUARE_1:def_2;
|.q.| = (abs (2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))))) * |.p.| by A77, TOPRNS_1:7;
then |.q.| * |.q.| = (((abs (2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))))) * (abs (2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|))))))) * |.p.|) * |.p.|
.= (((2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|))))) * (2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))))) * |.p.|) * |.p.| by A62
.= (((2 * 2) / ((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) * (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))))) * |.p.|) * |.p.| by XCMPLX_1:76
.= ((4 * |.p.|) * |.p.|) / ((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) ^2) ;
then A79: 1 - (|.q.| * |.q.|) = (((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) ^2) / ((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) ^2)) - (((4 * |.p.|) * |.p.|) / ((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) ^2)) by A78, XCMPLX_1:60
.= (((1 + (2 * (sqrt (1 + ((4 * |.p.|) * |.p.|))))) + ((sqrt (1 + ((4 * |.p.|) * |.p.|))) ^2)) - ((4 * |.p.|) * |.p.|)) / ((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) ^2)
.= (((1 + (2 * (sqrt (1 + ((4 * |.p.|) * |.p.|))))) + (1 + ((4 * |.p.|) * |.p.|))) - ((4 * |.p.|) * |.p.|)) / ((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) ^2) by SQUARE_1:def_2
.= (2 * (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|))))) / ((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) * (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))))
.= 2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) by A78, XCMPLX_1:91 ;
f . (f14 . x) = (1 / (2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))))) * q by A2, A79
.= ((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) / 2) * q by XCMPLX_1:57
.= (((1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))) / 2) * (2 / (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))))) * p by A77, EUCLID:30
.= ((2 * (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|))))) / (2 * (1 + (sqrt (1 + ((4 * |.p.|) * |.p.|)))))) * p by XCMPLX_1:76
.= 1 * p by A78, XCMPLX_1:60
.= p by EUCLID:29 ;
then [(f14 . x),x] in f by A76, FUNCT_1:def_2;
then [x,(f14 . x)] in g ~ by RELAT_1:def_7;
then [x,(f14 . x)] in g " by A35, FUNCT_1:def_5;
hence f14 . x = (f ") . x by A74, FUNCT_1:1; ::_thesis: verum
end;
then f " is continuous by A72, FUNCT_1:2, PRE_TOPC:27;
hence f is being_homeomorphism by A3, A14, A35, A44, A48, TOPS_2:def_5; ::_thesis: verum
end;
theorem Th7: :: MFOLD_1:7
for n being Nat
for p being Point of (TOP-REAL n)
for r being real positive number
for f being Function of (Tunit_ball n),(Tball (p,r)) st n <> 0 & ( for a being Point of (Tunit_ball n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (r * b) + p ) holds
f is being_homeomorphism
proof
let n be Nat; ::_thesis: for p being Point of (TOP-REAL n)
for r being real positive number
for f being Function of (Tunit_ball n),(Tball (p,r)) st n <> 0 & ( for a being Point of (Tunit_ball n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (r * b) + p ) holds
f is being_homeomorphism
let p be Point of (TOP-REAL n); ::_thesis: for r being real positive number
for f being Function of (Tunit_ball n),(Tball (p,r)) st n <> 0 & ( for a being Point of (Tunit_ball n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (r * b) + p ) holds
f is being_homeomorphism
let r be real positive number ; ::_thesis: for f being Function of (Tunit_ball n),(Tball (p,r)) st n <> 0 & ( for a being Point of (Tunit_ball n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (r * b) + p ) holds
f is being_homeomorphism
let f be Function of (Tunit_ball n),(Tball (p,r)); ::_thesis: ( n <> 0 & ( for a being Point of (Tunit_ball n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (r * b) + p ) implies f is being_homeomorphism )
assume that
A1: n <> 0 and
A2: for a being Point of (Tunit_ball n)
for b being Point of (TOP-REAL n) st a = b holds
f . a = (r * b) + p ; ::_thesis: f is being_homeomorphism
reconsider n1 = n as non empty Element of NAT by A1, ORDINAL1:def_12;
reconsider x = p as Point of (TOP-REAL n1) ;
defpred S1[ Point of (TOP-REAL n1), set ] means $2 = (r * $1) + x;
set U = Tunit_ball n;
set B = Tball (x,r);
A3: for u being Point of (TOP-REAL n1) ex y being Point of (TOP-REAL n1) st S1[u,y] ;
consider F being Function of (TOP-REAL n1),(TOP-REAL n1) such that
A4: for x being Point of (TOP-REAL n1) holds S1[x,F . x] from FUNCT_2:sch_3(A3);
defpred S2[ Point of (TOP-REAL n1), set ] means $2 = (1 / r) * ($1 - x);
A5: for u being Point of (TOP-REAL n1) ex y being Point of (TOP-REAL n1) st S2[u,y] ;
consider G being Function of (TOP-REAL n1),(TOP-REAL n1) such that
A6: for a being Point of (TOP-REAL n1) holds S2[a,G . a] from FUNCT_2:sch_3(A5);
set f2 = (TOP-REAL n1) --> x;
set f1 = id (TOP-REAL n1);
dom G = the carrier of (TOP-REAL n) by FUNCT_2:def_1;
then A7: dom (G | (Ball (x,r))) = Ball (x,r) by RELAT_1:62;
for p being Point of (TOP-REAL n1) holds G . p = ((1 / r) * ((id (TOP-REAL n1)) . p)) + ((- (1 / r)) * (((TOP-REAL n1) --> x) . p))
proof
let p be Point of (TOP-REAL n1); ::_thesis: G . p = ((1 / r) * ((id (TOP-REAL n1)) . p)) + ((- (1 / r)) * (((TOP-REAL n1) --> x) . p))
thus ((1 / r) * ((id (TOP-REAL n1)) . p)) + ((- (1 / r)) * (((TOP-REAL n1) --> x) . p)) = ((1 / r) * p) + ((- (1 / r)) * (((TOP-REAL n1) --> x) . p)) by FUNCT_1:18
.= ((1 / r) * p) + ((- (1 / r)) * x) by FUNCOP_1:7
.= ((1 / r) * p) - ((1 / r) * x) by EUCLID:40
.= (1 / r) * (p - x) by EUCLID:49
.= G . p by A6 ; ::_thesis: verum
end;
then A8: G is continuous by TOPALG_1:16;
A9: dom f = [#] (Tunit_ball n) by FUNCT_2:def_1;
A10: dom f = the carrier of (Tunit_ball n) by FUNCT_2:def_1;
for p being Point of (TOP-REAL n1) holds F . p = (r * ((id (TOP-REAL n1)) . p)) + (1 * (((TOP-REAL n1) --> x) . p))
proof
let p be Point of (TOP-REAL n1); ::_thesis: F . p = (r * ((id (TOP-REAL n1)) . p)) + (1 * (((TOP-REAL n1) --> x) . p))
thus (r * ((id (TOP-REAL n1)) . p)) + (1 * (((TOP-REAL n1) --> x) . p)) = (r * ((id (TOP-REAL n1)) . p)) + (((TOP-REAL n1) --> x) . p) by EUCLID:29
.= (r * p) + (((TOP-REAL n1) --> x) . p) by FUNCT_1:18
.= (r * p) + x by FUNCOP_1:7
.= F . p by A4 ; ::_thesis: verum
end;
then A11: F is continuous by TOPALG_1:16;
A12: the carrier of (Tball (x,r)) = Ball (x,r) by Th4;
A13: the carrier of (Tunit_ball n) = Ball ((0. (TOP-REAL n)),1) by Th4;
A14: for a being set st a in dom f holds
f . a = (F | (Ball ((0. (TOP-REAL n)),1))) . a
proof
let a be set ; ::_thesis: ( a in dom f implies f . a = (F | (Ball ((0. (TOP-REAL n)),1))) . a )
assume A15: a in dom f ; ::_thesis: f . a = (F | (Ball ((0. (TOP-REAL n)),1))) . a
reconsider y = a as Point of (TOP-REAL n1) by A15, PRE_TOPC:25;
thus f . a = (r * y) + x by A2, A15
.= F . y by A4
.= (F | (Ball ((0. (TOP-REAL n)),1))) . a by A13, A15, FUNCT_1:49 ; ::_thesis: verum
end;
A16: (1 / r) * r = 1 by XCMPLX_1:87;
A17: rng f = [#] (Tball (x,r))
proof
now__::_thesis:_for_b_being_set_st_b_in_[#]_(Tball_(x,r))_holds_
b_in_rng_f
let b be set ; ::_thesis: ( b in [#] (Tball (x,r)) implies b in rng f )
assume A18: b in [#] (Tball (x,r)) ; ::_thesis: b in rng f
then reconsider c = b as Point of (TOP-REAL n1) by PRE_TOPC:25;
reconsider r1 = 1 / r as Real ;
set a = r1 * (c - x);
A19: |.((r1 * (c - x)) - (0. (TOP-REAL n1))).| = |.(r1 * (c - x)).| by RLVECT_1:13
.= (abs r1) * |.(c - x).| by TOPRNS_1:7
.= r1 * |.(c - x).| by ABSVALUE:def_1 ;
|.(c - x).| < r by A12, A18, TOPREAL9:7;
then (1 / r) * |.(c - x).| < (1 / r) * r by XREAL_1:68;
then A20: r1 * (c - x) in Ball ((0. (TOP-REAL n)),1) by A16, A19;
then f . (r1 * (c - x)) = (r * (r1 * (c - x))) + x by A2, A13
.= ((r * (1 / r)) * (c - x)) + x by EUCLID:30
.= (c - x) + x by A16, EUCLID:29
.= b by EUCLID:48 ;
hence b in rng f by A13, A10, A20, FUNCT_1:def_3; ::_thesis: verum
end;
then [#] (Tball (x,r)) c= rng f by TARSKI:def_3;
hence rng f = [#] (Tball (x,r)) by XBOOLE_0:def_10; ::_thesis: verum
end;
now__::_thesis:_for_a,_b_being_set_st_a_in_dom_f_&_b_in_dom_f_&_f_._a_=_f_._b_holds_
a_=_b
let a, b be set ; ::_thesis: ( a in dom f & b in dom f & f . a = f . b implies a = b )
assume that
A21: a in dom f and
A22: b in dom f and
A23: f . a = f . b ; ::_thesis: a = b
reconsider a1 = a, b1 = b as Point of (TOP-REAL n1) by A13, A10, A21, A22;
A24: f . b1 = (r * b1) + x by A2, A22;
f . a1 = (r * a1) + x by A2, A21;
then r * a1 = ((r * b1) + x) - x by A23, A24, EUCLID:48;
hence a = b by EUCLID:34, EUCLID:48; ::_thesis: verum
end;
then A25: f is one-to-one by FUNCT_1:def_4;
A26: for a being set st a in dom (f ") holds
(f ") . a = (G | (Ball (x,r))) . a
proof
reconsider ff = f as Function ;
let a be set ; ::_thesis: ( a in dom (f ") implies (f ") . a = (G | (Ball (x,r))) . a )
assume A27: a in dom (f ") ; ::_thesis: (f ") . a = (G | (Ball (x,r))) . a
reconsider y = a as Point of (TOP-REAL n1) by A27, PRE_TOPC:25;
reconsider r1 = 1 / r as Real ;
set e = (1 / r) * (y - x);
A28: f is onto by A17, FUNCT_2:def_3;
A29: |.(((1 / r) * (y - x)) - (0. (TOP-REAL n1))).| = |.((1 / r) * (y - x)).| by RLVECT_1:13
.= (abs r1) * |.(y - x).| by TOPRNS_1:7
.= r1 * |.(y - x).| by ABSVALUE:def_1 ;
|.(y - x).| < r by A27, A12, TOPREAL9:7;
then (1 / r) * |.(y - x).| < (1 / r) * r by XREAL_1:68;
then A30: (1 / r) * (y - x) in Ball ((0. (TOP-REAL n)),1) by A16, A29;
then f . ((1 / r) * (y - x)) = (r * ((1 / r) * (y - x))) + x by A2, A13
.= ((r * (1 / r)) * (y - x)) + x by EUCLID:30
.= (y - x) + x by A16, EUCLID:29
.= y by EUCLID:48 ;
then (ff ") . a = (1 / r) * (y - x) by A13, A10, A25, A30, FUNCT_1:32;
hence (f ") . a = (1 / r) * (y - x) by A28, A25, TOPS_2:def_4
.= G . y by A6
.= (G | (Ball (x,r))) . a by A12, A27, FUNCT_1:49 ;
::_thesis: verum
end;
dom F = the carrier of (TOP-REAL n) by FUNCT_2:def_1;
then dom (F | (Ball ((0. (TOP-REAL n)),1))) = Ball ((0. (TOP-REAL n)),1) by RELAT_1:62;
then A31: f is continuous by A13, A10, A11, A14, BORSUK_4:44, FUNCT_1:2;
A32: dom (f ") = the carrier of (Tball (x,r)) by FUNCT_2:def_1;
f " is continuous by A32, A12, A7, A8, A26, BORSUK_4:44, FUNCT_1:2;
hence f is being_homeomorphism by A9, A17, A25, A31, TOPS_2:def_5; ::_thesis: verum
end;
theorem Th8: :: MFOLD_1:8
for n being Nat holds Tunit_ball n, TOP-REAL n are_homeomorphic
proof
let n be Nat; ::_thesis: Tunit_ball n, TOP-REAL n are_homeomorphic
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
set U = Tunit_ball n;
set C = TOP-REAL n;
percases ( not n is empty or n is empty ) ;
supposeA1: not n is empty ; ::_thesis: Tunit_ball n, TOP-REAL n are_homeomorphic
defpred S1[ Point of (Tunit_ball n), set ] means ex w being Point of (TOP-REAL n1) st
( w = $1 & $2 = (1 / (1 - (|.w.| * |.w.|))) * w );
A2: for u being Point of (Tunit_ball n) ex y being Point of (TOP-REAL n) st S1[u,y]
proof
let u be Point of (Tunit_ball n); ::_thesis: ex y being Point of (TOP-REAL n) st S1[u,y]
reconsider v = u as Point of (TOP-REAL n1) by PRE_TOPC:25;
set y = (1 / (1 - (|.v.| * |.v.|))) * v;
reconsider y = (1 / (1 - (|.v.| * |.v.|))) * v as Point of (TOP-REAL n) ;
take y ; ::_thesis: S1[u,y]
thus S1[u,y] ; ::_thesis: verum
end;
consider f being Function of (Tunit_ball n),(TOP-REAL n) such that
A3: for x being Point of (Tunit_ball n) holds S1[x,f . x] from FUNCT_2:sch_3(A2);
for a being Point of (Tunit_ball n)
for b being Point of (TOP-REAL n1) st a = b holds
f . a = (1 / (1 - (|.b.| * |.b.|))) * b
proof
let a be Point of (Tunit_ball n); ::_thesis: for b being Point of (TOP-REAL n1) st a = b holds
f . a = (1 / (1 - (|.b.| * |.b.|))) * b
let b be Point of (TOP-REAL n1); ::_thesis: ( a = b implies f . a = (1 / (1 - (|.b.| * |.b.|))) * b )
S1[a,f . a] by A3;
hence ( a = b implies f . a = (1 / (1 - (|.b.| * |.b.|))) * b ) ; ::_thesis: verum
end;
then ex f being Function of (Tunit_ball n),(TOP-REAL n) st f is being_homeomorphism by A1, Th6;
hence Tunit_ball n, TOP-REAL n are_homeomorphic by T_0TOPSP:def_1; ::_thesis: verum
end;
supposeA4: n is empty ; ::_thesis: Tunit_ball n, TOP-REAL n are_homeomorphic
A5: for x being set holds
( x in Ball ((0. (TOP-REAL 0)),1) iff x = 0. (TOP-REAL 0) )
proof
let x be set ; ::_thesis: ( x in Ball ((0. (TOP-REAL 0)),1) iff x = 0. (TOP-REAL 0) )
thus ( x in Ball ((0. (TOP-REAL 0)),1) implies x = 0. (TOP-REAL 0) ) ; ::_thesis: ( x = 0. (TOP-REAL 0) implies x in Ball ((0. (TOP-REAL 0)),1) )
assume x = 0. (TOP-REAL 0) ; ::_thesis: x in Ball ((0. (TOP-REAL 0)),1)
then reconsider p = x as Point of (TOP-REAL 0) ;
|.(p - (0. (TOP-REAL 0))).| < 1 by EUCLID_2:39;
hence x in Ball ((0. (TOP-REAL 0)),1) ; ::_thesis: verum
end;
[#] (TOP-REAL 0) = {(0. (TOP-REAL 0))} by EUCLID:22, EUCLID:77
.= Ball ((0. (TOP-REAL 0)),1) by A5, TARSKI:def_1 ;
hence Tunit_ball n, TOP-REAL n are_homeomorphic by A4, Th1; ::_thesis: verum
end;
end;
end;
theorem Th9: :: MFOLD_1:9
for n being Nat
for p, q being Point of (TOP-REAL n)
for r, s being real positive number holds Tball (p,r), Tball (q,s) are_homeomorphic
proof
let n be Nat; ::_thesis: for p, q being Point of (TOP-REAL n)
for r, s being real positive number holds Tball (p,r), Tball (q,s) are_homeomorphic
let p, q be Point of (TOP-REAL n); ::_thesis: for r, s being real positive number holds Tball (p,r), Tball (q,s) are_homeomorphic
let r, s be real positive number ; ::_thesis: Tball (p,r), Tball (q,s) are_homeomorphic
percases ( n is empty or not n is empty ) ;
supposeA1: n is empty ; ::_thesis: Tball (p,r), Tball (q,s) are_homeomorphic
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
reconsider p1 = p, q1 = q as Point of (TOP-REAL n1) ;
set X = { x where x is Point of (TOP-REAL n) : |.(x - p).| < r } ;
set Y = { x where x is Point of (TOP-REAL n) : |.(x - q).| < s } ;
A2: p1 = 0. (TOP-REAL 0) by A1;
A3: q1 = 0. (TOP-REAL 0) by A1;
for x being set holds
( x in { x where x is Point of (TOP-REAL n) : |.(x - p).| < r } iff x in { x where x is Point of (TOP-REAL n) : |.(x - q).| < s } )
proof
let x be set ; ::_thesis: ( x in { x where x is Point of (TOP-REAL n) : |.(x - p).| < r } iff x in { x where x is Point of (TOP-REAL n) : |.(x - q).| < s } )
hereby ::_thesis: ( x in { x where x is Point of (TOP-REAL n) : |.(x - q).| < s } implies x in { x where x is Point of (TOP-REAL n) : |.(x - p).| < r } )
assume x in { x where x is Point of (TOP-REAL n) : |.(x - p).| < r } ; ::_thesis: x in { x where x is Point of (TOP-REAL n) : |.(x - q).| < s }
then consider x1 being Point of (TOP-REAL n) such that
A4: ( x = x1 & |.(x1 - p).| < r ) ;
reconsider x1 = x1 as Point of (TOP-REAL n1) ;
x1 = 0. (TOP-REAL 0) by A1;
then |.(x1 - p1).| = 0 by A2, TOPRNS_1:28;
hence x in { x where x is Point of (TOP-REAL n) : |.(x - q).| < s } by A2, A3, A4; ::_thesis: verum
end;
assume x in { x where x is Point of (TOP-REAL n) : |.(x - q).| < s } ; ::_thesis: x in { x where x is Point of (TOP-REAL n) : |.(x - p).| < r }
then consider x1 being Point of (TOP-REAL n) such that
A5: ( x = x1 & |.(x1 - q).| < s ) ;
reconsider x1 = x1 as Point of (TOP-REAL n1) ;
x1 = 0. (TOP-REAL 0) by A1;
then |.(x1 - q1).| = 0 by A3, TOPRNS_1:28;
hence x in { x where x is Point of (TOP-REAL n) : |.(x - p).| < r } by A2, A3, A5; ::_thesis: verum
end;
hence Tball (p,r), Tball (q,s) are_homeomorphic by TARSKI:1; ::_thesis: verum
end;
suppose not n is empty ; ::_thesis: Tball (p,r), Tball (q,s) are_homeomorphic
then reconsider n1 = n as non empty Element of NAT by ORDINAL1:def_12;
A6: for r being real positive number
for x being Point of (TOP-REAL n1) holds Tunit_ball n1, Tball (x,r) are_homeomorphic
proof
let r be real positive number ; ::_thesis: for x being Point of (TOP-REAL n1) holds Tunit_ball n1, Tball (x,r) are_homeomorphic
let x be Point of (TOP-REAL n1); ::_thesis: Tunit_ball n1, Tball (x,r) are_homeomorphic
set U = Tunit_ball n;
set C = Tball (x,r);
defpred S1[ Point of (Tunit_ball n), set ] means ex w being Point of (TOP-REAL n1) st
( w = $1 & $2 = (r * w) + x );
A7: r is Real by XREAL_0:def_1;
A8: the carrier of (Tball (x,r)) = Ball (x,r) by Th4;
A9: for u being Point of (Tunit_ball n) ex y being Point of (Tball (x,r)) st S1[u,y]
proof
let u be Point of (Tunit_ball n); ::_thesis: ex y being Point of (Tball (x,r)) st S1[u,y]
reconsider v = u as Point of (TOP-REAL n1) by PRE_TOPC:25;
set y = (r * v) + x;
A10: |.(((r * v) + x) - x).| = |.(r * v).| by EUCLID:48
.= (abs r) * |.v.| by A7, TOPRNS_1:7
.= r * |.v.| by ABSVALUE:def_1 ;
r * |.v.| < r * 1 by Th5, XREAL_1:68;
then reconsider y = (r * v) + x as Point of (Tball (x,r)) by A10, A8, TOPREAL9:7;
take y ; ::_thesis: S1[u,y]
thus S1[u,y] ; ::_thesis: verum
end;
consider f being Function of (Tunit_ball n),(Tball (x,r)) such that
A11: for x being Point of (Tunit_ball n) holds S1[x,f . x] from FUNCT_2:sch_3(A9);
for a being Point of (Tunit_ball n)
for b being Point of (TOP-REAL n1) st a = b holds
f . a = (r * b) + x
proof
let a be Point of (Tunit_ball n); ::_thesis: for b being Point of (TOP-REAL n1) st a = b holds
f . a = (r * b) + x
let b be Point of (TOP-REAL n1); ::_thesis: ( a = b implies f . a = (r * b) + x )
S1[a,f . a] by A11;
hence ( a = b implies f . a = (r * b) + x ) ; ::_thesis: verum
end;
then ex f being Function of (Tunit_ball n),(Tball (x,r)) st f is being_homeomorphism by Th7;
hence Tunit_ball n1, Tball (x,r) are_homeomorphic by T_0TOPSP:def_1; ::_thesis: verum
end;
for x, y being Point of (TOP-REAL n1) holds Tball (x,r), Tball (y,s) are_homeomorphic
proof
let x, y be Point of (TOP-REAL n1); ::_thesis: Tball (x,r), Tball (y,s) are_homeomorphic
A12: Tunit_ball n, Tball (y,s) are_homeomorphic by A6;
Tball (x,r), Tunit_ball n are_homeomorphic by A6;
hence Tball (x,r), Tball (y,s) are_homeomorphic by A12, BORSUK_3:3; ::_thesis: verum
end;
hence Tball (p,r), Tball (q,s) are_homeomorphic ; ::_thesis: verum
end;
end;
end;
theorem Th10: :: MFOLD_1:10
for n being Nat
for B being non empty ball Subset of (TOP-REAL n) holds B, [#] (TOP-REAL n) are_homeomorphic
proof
let n be Nat; ::_thesis: for B being non empty ball Subset of (TOP-REAL n) holds B, [#] (TOP-REAL n) are_homeomorphic
let B be non empty ball Subset of (TOP-REAL n); ::_thesis: B, [#] (TOP-REAL n) are_homeomorphic
consider p being Point of (TOP-REAL n), r being real number such that
A1: B = Ball (p,r) by Def1;
reconsider B1 = Tball (p,r) as non empty TopSpace by A1;
A2: TOP-REAL n,(TOP-REAL n) | ([#] (TOP-REAL n)) are_homeomorphic by Th1;
A3: Tunit_ball n, TOP-REAL n are_homeomorphic by Th8;
r is positive by A1;
then Tball (p,r), Tball ((0. (TOP-REAL n)),1) are_homeomorphic by Th9;
then B1, TOP-REAL n are_homeomorphic by A3, BORSUK_3:3;
then Tball (p,r),(TOP-REAL n) | ([#] (TOP-REAL n)) are_homeomorphic by A2, BORSUK_3:3;
hence B, [#] (TOP-REAL n) are_homeomorphic by A1, METRIZTS:def_1; ::_thesis: verum
end;
theorem Th11: :: MFOLD_1:11
for M, N being non empty TopSpace
for p being Point of M
for U being a_neighborhood of p
for B being open Subset of N st U,B are_homeomorphic holds
ex V being open Subset of M ex S being open Subset of N st
( V c= U & p in V & V,S are_homeomorphic )
proof
let M, N be non empty TopSpace; ::_thesis: for p being Point of M
for U being a_neighborhood of p
for B being open Subset of N st U,B are_homeomorphic holds
ex V being open Subset of M ex S being open Subset of N st
( V c= U & p in V & V,S are_homeomorphic )
let p be Point of M; ::_thesis: for U being a_neighborhood of p
for B being open Subset of N st U,B are_homeomorphic holds
ex V being open Subset of M ex S being open Subset of N st
( V c= U & p in V & V,S are_homeomorphic )
let U be a_neighborhood of p; ::_thesis: for B being open Subset of N st U,B are_homeomorphic holds
ex V being open Subset of M ex S being open Subset of N st
( V c= U & p in V & V,S are_homeomorphic )
let B be open Subset of N; ::_thesis: ( U,B are_homeomorphic implies ex V being open Subset of M ex S being open Subset of N st
( V c= U & p in V & V,S are_homeomorphic ) )
assume U,B are_homeomorphic ; ::_thesis: ex V being open Subset of M ex S being open Subset of N st
( V c= U & p in V & V,S are_homeomorphic )
then A1: M | U,N | B are_homeomorphic by METRIZTS:def_1;
then consider f being Function of (M | U),(N | B) such that
A2: f is being_homeomorphism by T_0TOPSP:def_1;
consider V being Subset of M such that
A3: ( V is open & V c= U & p in V ) by CONNSP_2:6;
V c= [#] (M | U) by A3, PRE_TOPC:def_5;
then reconsider V1 = V as Subset of (M | U) ;
reconsider M1 = M | U as non empty TopStruct by A3;
reconsider N1 = N | B as non empty TopStruct by A3, A1, YELLOW14:18;
reconsider f1 = f as Function of M1,N1 ;
rng f c= [#] (N | B) ;
then A4: rng f c= B by PRE_TOPC:def_5;
V1,f .: V1 are_homeomorphic by A2, METRIZTS:3;
then A5: (M | U) | V1,(N | B) | (f .: V1) are_homeomorphic by METRIZTS:def_1;
reconsider V = V as open Subset of M by A3;
B = the carrier of (N | B) by PRE_TOPC:8;
then reconsider N1 = N | B as open SubSpace of N by TSEP_1:16;
B c= the carrier of N ;
then [#] (N | B) c= the carrier of N by PRE_TOPC:def_5;
then reconsider S = f .: V1 as Subset of N by XBOOLE_1:1;
reconsider S1 = f .: V1 as Subset of N1 ;
A6: for P being Subset of M1 holds
( P is open iff f1 .: P is open ) by A2, TOPGRP_1:25;
A7: V in the topology of M by PRE_TOPC:def_2;
V1 = V /\ ([#] M1) by XBOOLE_1:28;
then V1 in the topology of M1 by A7, PRE_TOPC:def_4;
then V1 is open by PRE_TOPC:def_2;
then S1 is open by A6;
then reconsider S = S as open Subset of N by TSEP_1:17;
take V ; ::_thesis: ex S being open Subset of N st
( V c= U & p in V & V,S are_homeomorphic )
take S ; ::_thesis: ( V c= U & p in V & V,S are_homeomorphic )
thus ( V c= U & p in V ) by A3; ::_thesis: V,S are_homeomorphic
A8: (M | U) | V1 = M | V by A3, PRE_TOPC:7;
f .: U c= rng f by RELAT_1:111;
then A9: f .: U c= B by A4, XBOOLE_1:1;
f .: V c= f .: U by A3, RELAT_1:123;
then (N | B) | (f .: V1) = N | S by A9, PRE_TOPC:7, XBOOLE_1:1;
hence V,S are_homeomorphic by A5, A8, METRIZTS:def_1; ::_thesis: verum
end;
begin
definition
let n be Nat;
let M be non empty TopSpace;
attrM is n -locally_euclidean means :Def4: :: MFOLD_1:def 4
for p being Point of M ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic ;
end;
:: deftheorem Def4 defines -locally_euclidean MFOLD_1:def_4_:_
for n being Nat
for M being non empty TopSpace holds
( M is n -locally_euclidean iff for p being Point of M ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic );
registration
let n be Nat;
cluster TOP-REAL n -> n -locally_euclidean ;
coherence
TOP-REAL n is n -locally_euclidean
proof
let p be Point of (TOP-REAL n); :: according to MFOLD_1:def_4 ::_thesis: ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic
p in [#] (TOP-REAL n) ;
then p in Int ([#] (TOP-REAL n)) by TOPS_1:15;
then reconsider U = [#] (TOP-REAL n) as a_neighborhood of p by CONNSP_2:def_1;
reconsider S = U as open Subset of (TOP-REAL n) ;
take U ; ::_thesis: ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic
take S ; ::_thesis: U,S are_homeomorphic
thus U,S are_homeomorphic by METRIZTS:1; ::_thesis: verum
end;
end;
registration
let n be Nat;
cluster non empty TopSpace-like n -locally_euclidean for TopStruct ;
correctness
existence
ex b1 being non empty TopSpace st b1 is n -locally_euclidean ;
proof
take TOP-REAL n ; ::_thesis: TOP-REAL n is n -locally_euclidean
thus TOP-REAL n is n -locally_euclidean ; ::_thesis: verum
end;
end;
Lm1: for n being Nat
for M being non empty TopSpace st M is n -locally_euclidean holds
for p being Point of M ex U being a_neighborhood of p ex B being non empty ball Subset of (TOP-REAL n) st U,B are_homeomorphic
proof
let n be Nat; ::_thesis: for M being non empty TopSpace st M is n -locally_euclidean holds
for p being Point of M ex U being a_neighborhood of p ex B being non empty ball Subset of (TOP-REAL n) st U,B are_homeomorphic
let M be non empty TopSpace; ::_thesis: ( M is n -locally_euclidean implies for p being Point of M ex U being a_neighborhood of p ex B being non empty ball Subset of (TOP-REAL n) st U,B are_homeomorphic )
assume A1: M is n -locally_euclidean ; ::_thesis: for p being Point of M ex U being a_neighborhood of p ex B being non empty ball Subset of (TOP-REAL n) st U,B are_homeomorphic
let p be Point of M; ::_thesis: ex U being a_neighborhood of p ex B being non empty ball Subset of (TOP-REAL n) st U,B are_homeomorphic
consider U being a_neighborhood of p, S being open Subset of (TOP-REAL n) such that
A2: U,S are_homeomorphic by A1, Def4;
consider U1 being open Subset of M, S being open Subset of (TOP-REAL n) such that
A3: ( U1 c= U & p in U1 & U1,S are_homeomorphic ) by A2, Th11;
reconsider U1 = U1 as non empty Subset of M by A3;
A4: M | U1,(TOP-REAL n) | S are_homeomorphic by A3, METRIZTS:def_1;
then consider f being Function of (M | U1),((TOP-REAL n) | S) such that
A5: f is being_homeomorphism by T_0TOPSP:def_1;
A6: p in [#] (M | U1) by A3, PRE_TOPC:def_5;
reconsider S1 = (TOP-REAL n) | S as non empty TopSpace by A4, YELLOW14:18;
reconsider M1 = M | U1 as non empty SubSpace of M ;
reconsider f = f as Function of M1,S1 ;
A7: [#] ((TOP-REAL n) | S) = S by PRE_TOPC:def_5;
A8: [#] ((TOP-REAL n) | S) c= [#] (TOP-REAL n) by PRE_TOPC:def_4;
f . p in the carrier of ((TOP-REAL n) | S) by A6, FUNCT_2:5;
then reconsider q = f . p as Point of (TOP-REAL n) by A8;
consider B being ball Subset of (TOP-REAL n) such that
A9: ( B c= S & q in B ) by A6, A7, Th3, FUNCT_2:5;
reconsider B = B as non empty ball Subset of (TOP-REAL n) by A9;
A10: f " is being_homeomorphism by A5, TOPS_2:56;
reconsider B1 = B as non empty Subset of S1 by A9, A7;
A11: rng f = [#] S1 by A5, TOPS_2:def_5;
A12: f is one-to-one by A5, TOPS_2:def_5;
A13: dom (f ") = the carrier of S1 by A11, A12, TOPS_2:49;
then A14: (f ") . q in (f ") .: B1 by A9, FUNCT_1:def_6;
then reconsider U2 = (f ") .: B1 as non empty Subset of M1 ;
A15: dom ((f ") | B1) = B1 by A13, RELAT_1:62;
A16: dom ((f ") | B1) = [#] (S1 | B1) by A15, PRE_TOPC:def_5
.= the carrier of (S1 | B1) ;
rng ((f ") | B1) = (f ") .: B1 by RELAT_1:115
.= [#] (M1 | U2) by PRE_TOPC:def_5
.= the carrier of (M1 | U2) ;
then reconsider g = (f ") | B1 as Function of (S1 | B1),(M1 | U2) by A16, FUNCT_2:1;
A17: g is being_homeomorphism by A10, METRIZTS:2;
reconsider p1 = p as Point of M1 by A6;
reconsider f1 = f as Function ;
A18: ( f1 is one-to-one & p in dom f1 ) by A5, A6, TOPS_2:def_5;
f is onto by A11, FUNCT_2:def_3;
then f1 " = f " by A12, TOPS_2:def_4;
then A19: p1 in U2 by A14, A18, FUNCT_1:34;
A20: [#] M1 c= [#] M by PRE_TOPC:def_4;
reconsider V = U2 as Subset of M by A20, XBOOLE_1:1;
A21: B in the topology of (TOP-REAL n) by PRE_TOPC:def_2;
B1 = B /\ ([#] S1) by XBOOLE_1:28;
then B1 in the topology of S1 by A21, PRE_TOPC:def_4;
then B1 is open by PRE_TOPC:def_2;
then (f ") .: B1 is open by A10, TOPGRP_1:25;
then reconsider V = V as a_neighborhood of p by A19, CONNSP_2:3, CONNSP_2:9;
take V ; ::_thesis: ex B being non empty ball Subset of (TOP-REAL n) st V,B are_homeomorphic
take B ; ::_thesis: V,B are_homeomorphic
A22: M1 | U2,S1 | B1 are_homeomorphic by A17, T_0TOPSP:def_1;
rng (f ") c= [#] (M | U1) ;
then A23: rng (f ") c= U1 by PRE_TOPC:def_5;
(f ") .: B1 c= rng (f ") by RELAT_1:111;
then A24: M | V = M1 | U2 by A23, PRE_TOPC:7, XBOOLE_1:1;
S1 | B1 = (TOP-REAL n) | B by A9, PRE_TOPC:7;
hence V,B are_homeomorphic by A24, A22, METRIZTS:def_1; ::_thesis: verum
end;
theorem :: MFOLD_1:12
for n being Nat
for M being non empty TopSpace holds
( M is n -locally_euclidean iff for p being Point of M ex U being a_neighborhood of p ex B being ball Subset of (TOP-REAL n) st U,B are_homeomorphic )
proof
let n be Nat; ::_thesis: for M being non empty TopSpace holds
( M is n -locally_euclidean iff for p being Point of M ex U being a_neighborhood of p ex B being ball Subset of (TOP-REAL n) st U,B are_homeomorphic )
let M be non empty TopSpace; ::_thesis: ( M is n -locally_euclidean iff for p being Point of M ex U being a_neighborhood of p ex B being ball Subset of (TOP-REAL n) st U,B are_homeomorphic )
hereby ::_thesis: ( ( for p being Point of M ex U being a_neighborhood of p ex B being ball Subset of (TOP-REAL n) st U,B are_homeomorphic ) implies M is n -locally_euclidean )
assume A1: M is n -locally_euclidean ; ::_thesis: for p being Point of M ex U being a_neighborhood of p ex B being ball Subset of (TOP-REAL n) st U,B are_homeomorphic
let p be Point of M; ::_thesis: ex U being a_neighborhood of p ex B being ball Subset of (TOP-REAL n) st U,B are_homeomorphic
consider U being a_neighborhood of p, B being non empty ball Subset of (TOP-REAL n) such that
A2: U,B are_homeomorphic by A1, Lm1;
reconsider B = B as ball Subset of (TOP-REAL n) ;
take U = U; ::_thesis: ex B being ball Subset of (TOP-REAL n) st U,B are_homeomorphic
take B = B; ::_thesis: U,B are_homeomorphic
thus U,B are_homeomorphic by A2; ::_thesis: verum
end;
assume A3: for p being Point of M ex U being a_neighborhood of p ex B being ball Subset of (TOP-REAL n) st U,B are_homeomorphic ; ::_thesis: M is n -locally_euclidean
now__::_thesis:_for_p_being_Point_of_M_ex_U_being_a_neighborhood_of_p_ex_S_being_open_Subset_of_(TOP-REAL_n)_st_U,S_are_homeomorphic
let p be Point of M; ::_thesis: ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic
consider U being a_neighborhood of p, B being ball Subset of (TOP-REAL n) such that
A4: U,B are_homeomorphic by A3;
reconsider S = B as open Subset of (TOP-REAL n) ;
take U = U; ::_thesis: ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic
take S = S; ::_thesis: U,S are_homeomorphic
thus U,S are_homeomorphic by A4; ::_thesis: verum
end;
hence M is n -locally_euclidean by Def4; ::_thesis: verum
end;
theorem Th13: :: MFOLD_1:13
for n being Nat
for M being non empty TopSpace holds
( M is n -locally_euclidean iff for p being Point of M ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic )
proof
let n be Nat; ::_thesis: for M being non empty TopSpace holds
( M is n -locally_euclidean iff for p being Point of M ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic )
let M be non empty TopSpace; ::_thesis: ( M is n -locally_euclidean iff for p being Point of M ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic )
hereby ::_thesis: ( ( for p being Point of M ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic ) implies M is n -locally_euclidean )
assume A1: M is n -locally_euclidean ; ::_thesis: for p being Point of M ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic
let p be Point of M; ::_thesis: ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic
consider U being a_neighborhood of p, B being non empty ball Subset of (TOP-REAL n) such that
A2: U,B are_homeomorphic by A1, Lm1;
take U = U; ::_thesis: U, [#] (TOP-REAL n) are_homeomorphic
A3: (TOP-REAL n) | ([#] (TOP-REAL n)) = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by TSEP_1:93;
reconsider B1 = (TOP-REAL n) | B as non empty TopSpace ;
M | U,B1 are_homeomorphic by A2, METRIZTS:def_1;
then reconsider U1 = M | U as non empty TopSpace by YELLOW14:18;
A4: U1,B1 are_homeomorphic by A2, METRIZTS:def_1;
B, [#] (TOP-REAL n) are_homeomorphic by Th10;
then A5: B1, TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) are_homeomorphic by A3, METRIZTS:def_1;
U1, TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) are_homeomorphic by A4, A5, BORSUK_3:3;
hence U, [#] (TOP-REAL n) are_homeomorphic by A3, METRIZTS:def_1; ::_thesis: verum
end;
assume A6: for p being Point of M ex U being a_neighborhood of p st U, [#] (TOP-REAL n) are_homeomorphic ; ::_thesis: M is n -locally_euclidean
now__::_thesis:_for_p_being_Point_of_M_ex_U_being_a_neighborhood_of_p_ex_S_being_open_Subset_of_(TOP-REAL_n)_st_U,S_are_homeomorphic
let p be Point of M; ::_thesis: ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic
consider U being a_neighborhood of p such that
A7: U, [#] (TOP-REAL n) are_homeomorphic by A6;
set S = the non empty ball Subset of (TOP-REAL n);
A8: the non empty ball Subset of (TOP-REAL n), [#] (TOP-REAL n) are_homeomorphic by Th10;
reconsider S = the non empty ball Subset of (TOP-REAL n) as open Subset of (TOP-REAL n) ;
take U = U; ::_thesis: ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic
take S = S; ::_thesis: U,S are_homeomorphic
A9: (TOP-REAL n) | ([#] (TOP-REAL n)) = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by TSEP_1:93;
A10: M | U, TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) are_homeomorphic by A7, A9, METRIZTS:def_1;
then reconsider U1 = M | U as non empty TopSpace by YELLOW14:18;
reconsider S1 = (TOP-REAL n) | S as non empty TopSpace ;
A11: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #),S1 are_homeomorphic by A8, A9, METRIZTS:def_1;
U1,S1 are_homeomorphic by A10, A11, BORSUK_3:3;
hence U,S are_homeomorphic by METRIZTS:def_1; ::_thesis: verum
end;
hence M is n -locally_euclidean by Def4; ::_thesis: verum
end;
registration
let n be Nat;
cluster non empty TopSpace-like n -locally_euclidean -> non empty first-countable for TopStruct ;
correctness
coherence
for b1 being non empty TopSpace st b1 is n -locally_euclidean holds
b1 is first-countable ;
proof
let M be non empty TopSpace; ::_thesis: ( M is n -locally_euclidean implies M is first-countable )
assume A1: M is n -locally_euclidean ; ::_thesis: M is first-countable
for p being Point of M ex B being Basis of p st B is countable
proof
let p be Point of M; ::_thesis: ex B being Basis of p st B is countable
consider U being a_neighborhood of p such that
A2: U, [#] (TOP-REAL n) are_homeomorphic by A1, Th13;
M | U,(TOP-REAL n) | ([#] (TOP-REAL n)) are_homeomorphic by A2, METRIZTS:def_1;
then M | U, TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) are_homeomorphic by TSEP_1:93;
then consider f being Function of (M | U),TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) such that
A3: f is being_homeomorphism by T_0TOPSP:def_1;
A4: ( dom f = [#] (M | U) & rng f = [#] TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) & f is one-to-one & f is continuous & f " is continuous ) by A3, TOPS_2:def_5;
then A5: dom f = U by PRE_TOPC:def_5;
A6: f is onto by A4, FUNCT_2:def_3;
A7: Int U c= U by TOPS_1:16;
A8: p in Int U by CONNSP_2:def_1;
A9: p in dom f by A8, A7, A5;
f . p in rng f by A8, A7, A5, FUNCT_1:3;
then reconsider q = f . p as Point of (TOP-REAL n) ;
reconsider n1 = n as Element of NAT by ORDINAL1:def_12;
TOP-REAL n1 is first-countable ;
then consider B1 being Basis of q such that
A10: B1 is countable by FRECHET:def_2;
reconsider A = bool the carrier of (TOP-REAL n) as non empty set ;
deffunc H1( set ) -> Element of bool the carrier of M = ((f ") .: n) /\ (Int U);
set B = { H1(X) where X is Element of A : X in B1 } ;
A11: card B1 c= omega by A10, CARD_3:def_14;
card { H1(X) where X is Element of A : X in B1 } c= card B1 from TREES_2:sch_2();
then A12: card { H1(X) where X is Element of A : X in B1 } c= omega by A11, XBOOLE_1:1;
for x being set st x in { H1(X) where X is Element of A : X in B1 } holds
x in bool the carrier of M
proof
let x be set ; ::_thesis: ( x in { H1(X) where X is Element of A : X in B1 } implies x in bool the carrier of M )
assume x in { H1(X) where X is Element of A : X in B1 } ; ::_thesis: x in bool the carrier of M
then consider X1 being Element of A such that
A13: ( x = H1(X1) & X1 in B1 ) ;
thus x in bool the carrier of M by A13; ::_thesis: verum
end;
then reconsider B = { H1(X) where X is Element of A : X in B1 } as Subset-Family of M by TARSKI:def_3;
A14: for P being Subset of M st P in B holds
P is open
proof
let P be Subset of M; ::_thesis: ( P in B implies P is open )
assume P in B ; ::_thesis: P is open
then consider X1 being Element of A such that
A15: ( P = H1(X1) & X1 in B1 ) ;
reconsider X1 = X1 as Subset of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) ;
reconsider X2 = X1 as Subset of (TOP-REAL n) ;
X2 is open by A15, YELLOW_8:12;
then X2 in the topology of (TOP-REAL n) by PRE_TOPC:def_2;
then A16: X1 is open by PRE_TOPC:def_2;
reconsider U1 = M | U as non empty TopStruct by A8, A7;
reconsider g = f " as Function of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #),U1 ;
A17: g is being_homeomorphism by A3, TOPS_2:56;
A18: g .: X1 is open by A16, A17, TOPGRP_1:25;
g .: X1 in the topology of (M | U) by A18, PRE_TOPC:def_2;
then consider Q being Subset of M such that
A19: ( Q in the topology of M & g .: X1 = Q /\ ([#] (M | U)) ) by PRE_TOPC:def_4;
[#] (M | U) = U by PRE_TOPC:def_5;
then A20: P = Q /\ (U /\ (Int U)) by A19, A15, XBOOLE_1:16
.= Q /\ (Int U) by TOPS_1:16, XBOOLE_1:28 ;
Q is open by A19, PRE_TOPC:def_2;
hence P is open by A20; ::_thesis: verum
end;
for Y being set st Y in B holds
p in Y
proof
let Y be set ; ::_thesis: ( Y in B implies p in Y )
assume Y in B ; ::_thesis: p in Y
then consider X1 being Element of A such that
A21: ( Y = H1(X1) & X1 in B1 ) ;
reconsider g = f as Function ;
[p,(g . p)] in g by A8, A7, A5, FUNCT_1:def_2;
then [q,p] in g ~ by RELAT_1:def_7;
then [q,p] in g " by A4, FUNCT_1:def_5;
then A22: [q,p] in f " by A6, A4, TOPS_2:def_4;
q in X1 by A21, YELLOW_8:12;
then p in (f ") .: X1 by A22, RELAT_1:def_13;
hence p in Y by A21, A8, XBOOLE_0:def_4; ::_thesis: verum
end;
then A23: p in Intersect B by SETFAM_1:43;
for S being Subset of M st S is open & p in S holds
ex V being Subset of M st
( V in B & V c= S )
proof
let S be Subset of M; ::_thesis: ( S is open & p in S implies ex V being Subset of M st
( V in B & V c= S ) )
assume A24: ( S is open & p in S ) ; ::_thesis: ex V being Subset of M st
( V in B & V c= S )
set S1 = S /\ ([#] (M | U));
S in the topology of M by A24, PRE_TOPC:def_2;
then A25: S /\ ([#] (M | U)) in the topology of (M | U) by PRE_TOPC:def_4;
reconsider U1 = M | U as non empty TopStruct by A8, A7;
reconsider S1 = S /\ ([#] (M | U)) as Subset of U1 ;
S1 is open by A25, PRE_TOPC:def_2;
then A26: f .: S1 is open by A3, TOPGRP_1:25;
reconsider S2 = f .: S1 as Subset of (TOP-REAL n) ;
f .: S1 in the topology of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by A26, PRE_TOPC:def_2;
then A27: S2 is open by PRE_TOPC:def_2;
reconsider g1 = f as Function ;
A28: [p,q] in f by A8, A7, A5, FUNCT_1:def_2;
p in S1 by A9, A24, XBOOLE_0:def_4;
then A29: q in S2 by A28, RELAT_1:def_13;
consider W being Subset of (TOP-REAL n) such that
A30: ( W in B1 & W c= S2 ) by A29, A27, YELLOW_8:13;
reconsider W = W as Element of A ;
set V = ((f ") .: W) /\ (Int U);
reconsider V = ((f ") .: W) /\ (Int U) as Subset of M ;
take V ; ::_thesis: ( V in B & V c= S )
thus V in B by A30; ::_thesis: V c= S
A31: g1 " = f " by A6, A4, TOPS_2:def_4;
A32: (f ") .: (f .: S1) = S1 by A31, A4, FUNCT_1:107;
A33: ((f ") .: W) /\ (Int U) c= (f ") .: W by XBOOLE_1:17;
A34: S1 c= S by XBOOLE_1:17;
(f ") .: W c= (f ") .: (f .: S1) by A30, RELAT_1:123;
then (f ") .: W c= S by A32, A34, XBOOLE_1:1;
hence V c= S by A33, XBOOLE_1:1; ::_thesis: verum
end;
then reconsider B = B as Basis of p by A14, A23, TOPS_2:def_1, YELLOW_8:def_1;
take B ; ::_thesis: B is countable
thus B is countable by A12, CARD_3:def_14; ::_thesis: verum
end;
hence M is first-countable by FRECHET:def_2; ::_thesis: verum
end;
end;
set T = (TOP-REAL 0) | ([#] (TOP-REAL 0));
Lm2: (TOP-REAL 0) | ([#] (TOP-REAL 0)) = TopStruct(# the carrier of (TOP-REAL 0), the topology of (TOP-REAL 0) #)
by TSEP_1:93;
registration
cluster non empty TopSpace-like 0 -locally_euclidean -> non empty discrete for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is 0 -locally_euclidean holds
b1 is discrete
proof
let M be non empty TopSpace; ::_thesis: ( M is 0 -locally_euclidean implies M is discrete )
assume A1: M is 0 -locally_euclidean ; ::_thesis: M is discrete
for X being Subset of M
for p being Point of M st X = {p} holds
X is open
proof
let X be Subset of M; ::_thesis: for p being Point of M st X = {p} holds
X is open
let p be Point of M; ::_thesis: ( X = {p} implies X is open )
assume A2: X = {p} ; ::_thesis: X is open
consider U being a_neighborhood of p such that
A3: U, [#] (TOP-REAL 0) are_homeomorphic by A1, Th13;
A4: Int U c= U by TOPS_1:16;
p in Int U by CONNSP_2:def_1;
then A5: p in U by A4;
M | U,(TOP-REAL 0) | ([#] (TOP-REAL 0)) are_homeomorphic by A3, METRIZTS:def_1;
then consider f being Function of (M | U),((TOP-REAL 0) | ([#] (TOP-REAL 0))) such that
A6: f is being_homeomorphism by T_0TOPSP:def_1;
consider V being Subset of M such that
A7: ( V is open & V c= U & p in V ) by CONNSP_2:6;
for x being set holds
( x in V iff x = p )
proof
let x be set ; ::_thesis: ( x in V iff x = p )
hereby ::_thesis: ( x = p implies x in V )
assume x in V ; ::_thesis: x = p
then A8: x in U by A7;
A9: f is one-to-one by A6, TOPS_2:def_5;
x in [#] (M | U) by A8, PRE_TOPC:def_5;
then A10: x in dom f by A6, TOPS_2:def_5;
then A11: f . x in rng f by FUNCT_1:3;
p in [#] (M | U) by A5, PRE_TOPC:def_5;
then A12: p in dom f by A6, TOPS_2:def_5;
then A13: f . p in rng f by FUNCT_1:3;
f . x = 0. (TOP-REAL 0) by Lm2, A11
.= f . p by Lm2, A13 ;
hence x = p by A9, A10, A12, FUNCT_1:def_4; ::_thesis: verum
end;
assume x = p ; ::_thesis: x in V
hence x in V by A7; ::_thesis: verum
end;
hence X is open by A2, A7, TARSKI:def_1; ::_thesis: verum
end;
hence M is discrete by TDLAT_3:17; ::_thesis: verum
end;
cluster non empty TopSpace-like discrete -> non empty 0 -locally_euclidean for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is discrete holds
b1 is 0 -locally_euclidean
proof
A14: [#] ((TOP-REAL 0) | ([#] (TOP-REAL 0))) = {(0. (TOP-REAL 0))} by Lm2, EUCLID:22, EUCLID:77;
let M be non empty TopSpace; ::_thesis: ( M is discrete implies M is 0 -locally_euclidean )
assume A15: M is discrete ; ::_thesis: M is 0 -locally_euclidean
for p being Point of M ex U being a_neighborhood of p st U, [#] (TOP-REAL 0) are_homeomorphic
proof
let p be Point of M; ::_thesis: ex U being a_neighborhood of p st U, [#] (TOP-REAL 0) are_homeomorphic
reconsider U = {p} as Subset of M by ZFMISC_1:31;
A16: ( U is open & p in U ) by A15, TARSKI:def_1, TDLAT_3:15;
then reconsider U = U as a_neighborhood of p by CONNSP_2:3;
take U ; ::_thesis: U, [#] (TOP-REAL 0) are_homeomorphic
set f = {[p,(0. (TOP-REAL 0))]};
A17: p in [#] (M | U) by A16, PRE_TOPC:def_5;
A18: [p,(0. (TOP-REAL 0))] in [: the carrier of (M | U), the carrier of ((TOP-REAL 0) | ([#] (TOP-REAL 0))):] by A17, Lm2, ZFMISC_1:87;
A19: dom {[p,(0. (TOP-REAL 0))]} = U by RELAT_1:9;
then A20: dom {[p,(0. (TOP-REAL 0))]} = [#] (M | U) by PRE_TOPC:def_5;
then reconsider f = {[p,(0. (TOP-REAL 0))]} as Function of (M | U),((TOP-REAL 0) | ([#] (TOP-REAL 0))) by A18, FUNCT_2:def_1, ZFMISC_1:31;
A21: rng f = [#] ((TOP-REAL 0) | ([#] (TOP-REAL 0))) by A14, RELAT_1:9;
for P being Subset of (M | U) holds
( P is closed iff f .: P is closed )
proof
let P be Subset of (M | U); ::_thesis: ( P is closed iff f .: P is closed )
percases ( P is empty or not P is empty ) ;
supposeA22: P is empty ; ::_thesis: ( P is closed iff f .: P is closed )
thus ( P is closed iff f .: P is closed ) by A22; ::_thesis: verum
end;
supposeA23: not P is empty ; ::_thesis: ( P is closed iff f .: P is closed )
then P = [#] (M | U) by A20, A19, ZFMISC_1:33;
hence ( P is closed implies f .: P is closed ) by A21, A20, RELAT_1:113; ::_thesis: ( f .: P is closed implies P is closed )
thus ( f .: P is closed implies P is closed ) by A23, A20, A19, ZFMISC_1:33; ::_thesis: verum
end;
end;
end;
then f is being_homeomorphism by A20, A21, TOPS_2:58;
then M | U,(TOP-REAL 0) | ([#] (TOP-REAL 0)) are_homeomorphic by T_0TOPSP:def_1;
hence U, [#] (TOP-REAL 0) are_homeomorphic by METRIZTS:def_1; ::_thesis: verum
end;
hence M is 0 -locally_euclidean by Th13; ::_thesis: verum
end;
end;
registration
let n be Nat;
cluster TOP-REAL n -> second-countable ;
correctness
coherence
TOP-REAL n is second-countable ;
proof
set T = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #);
A1: for x being set holds
( x in { (card B) where B is Basis of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) : verum } iff x in { (card B) where B is Basis of (TOP-REAL n) : verum } )
proof
let x be set ; ::_thesis: ( x in { (card B) where B is Basis of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) : verum } iff x in { (card B) where B is Basis of (TOP-REAL n) : verum } )
hereby ::_thesis: ( x in { (card B) where B is Basis of (TOP-REAL n) : verum } implies x in { (card B) where B is Basis of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) : verum } )
assume x in { (card B) where B is Basis of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) : verum } ; ::_thesis: x in { (card B) where B is Basis of (TOP-REAL n) : verum }
then consider B1 being Basis of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) such that
A2: x = card B1 ;
reconsider B2 = B1 as Basis of (TOP-REAL n) by YELLOW12:32;
x = card B2 by A2;
hence x in { (card B) where B is Basis of (TOP-REAL n) : verum } ; ::_thesis: verum
end;
assume x in { (card B) where B is Basis of (TOP-REAL n) : verum } ; ::_thesis: x in { (card B) where B is Basis of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) : verum }
then consider B1 being Basis of (TOP-REAL n) such that
A3: x = card B1 ;
reconsider B2 = B1 as Basis of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by YELLOW12:32;
x = card B2 by A3;
hence x in { (card B) where B is Basis of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) : verum } ; ::_thesis: verum
end;
weight TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = weight (TOP-REAL n) by A1, TARSKI:1;
then weight (TOP-REAL n) c= omega by WAYBEL23:def_6;
hence TOP-REAL n is second-countable by WAYBEL23:def_6; ::_thesis: verum
end;
end;
registration
let n be Nat;
cluster non empty TopSpace-like Hausdorff second-countable n -locally_euclidean for TopStruct ;
existence
ex b1 being non empty TopSpace st
( b1 is second-countable & b1 is Hausdorff & b1 is n -locally_euclidean )
proof
take TOP-REAL n ; ::_thesis: ( TOP-REAL n is second-countable & TOP-REAL n is Hausdorff & TOP-REAL n is n -locally_euclidean )
thus ( TOP-REAL n is second-countable & TOP-REAL n is Hausdorff & TOP-REAL n is n -locally_euclidean ) ; ::_thesis: verum
end;
end;
definition
let n be Nat;
let M be non empty TopSpace;
attrM is n -manifold means :Def5: :: MFOLD_1:def 5
( M is second-countable & M is Hausdorff & M is n -locally_euclidean );
end;
:: deftheorem Def5 defines -manifold MFOLD_1:def_5_:_
for n being Nat
for M being non empty TopSpace holds
( M is n -manifold iff ( M is second-countable & M is Hausdorff & M is n -locally_euclidean ) );
definition
let M be non empty TopSpace;
attrM is manifold-like means :Def6: :: MFOLD_1:def 6
ex n being Nat st M is n -manifold ;
end;
:: deftheorem Def6 defines manifold-like MFOLD_1:def_6_:_
for M being non empty TopSpace holds
( M is manifold-like iff ex n being Nat st M is n -manifold );
registration
let n be Nat;
cluster non empty TopSpace-like n -manifold for TopStruct ;
existence
ex b1 being non empty TopSpace st b1 is n -manifold
proof
take TOP-REAL n ; ::_thesis: TOP-REAL n is n -manifold
thus TOP-REAL n is n -manifold by Def5; ::_thesis: verum
end;
end;
registration
let n be Nat;
cluster non empty TopSpace-like n -manifold -> non empty Hausdorff second-countable n -locally_euclidean for TopStruct ;
correctness
coherence
for b1 being non empty TopSpace st b1 is n -manifold holds
( b1 is second-countable & b1 is Hausdorff & b1 is n -locally_euclidean );
by Def5;
cluster non empty TopSpace-like Hausdorff second-countable n -locally_euclidean -> non empty n -manifold for TopStruct ;
correctness
coherence
for b1 being non empty TopSpace st b1 is second-countable & b1 is Hausdorff & b1 is n -locally_euclidean holds
b1 is n -manifold ;
by Def5;
cluster non empty TopSpace-like n -manifold -> non empty manifold-like for TopStruct ;
correctness
coherence
for b1 being non empty TopSpace st b1 is n -manifold holds
b1 is manifold-like ;
by Def6;
end;
registration
cluster non empty TopSpace-like second-countable discrete -> non empty 0 -manifold for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is second-countable & b1 is discrete holds
b1 is 0 -manifold ;
end;
registration
let n be Nat;
let M be non empty n -manifold TopSpace;
cluster non empty open -> non empty n -manifold for SubSpace of M;
correctness
coherence
for b1 being non empty SubSpace of M st b1 is open holds
b1 is n -manifold ;
proof
let X be non empty SubSpace of M; ::_thesis: ( X is open implies X is n -manifold )
assume A1: X is open ; ::_thesis: X is n -manifold
[#] X c= [#] M by PRE_TOPC:def_4;
then reconsider X1 = [#] X as non empty open Subset of M by A1, TSEP_1:def_1;
A2: the carrier of X = [#] (M | X1) by PRE_TOPC:def_5
.= the carrier of (M | X1) ;
then A3: TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of (M | X1), the topology of (M | X1) #) by TSEP_1:5;
A4: for x being set holds
( x in { (card B) where B is Basis of X : verum } iff x in { (card B) where B is Basis of (M | X1) : verum } )
proof
let x be set ; ::_thesis: ( x in { (card B) where B is Basis of X : verum } iff x in { (card B) where B is Basis of (M | X1) : verum } )
hereby ::_thesis: ( x in { (card B) where B is Basis of (M | X1) : verum } implies x in { (card B) where B is Basis of X : verum } )
assume x in { (card B) where B is Basis of X : verum } ; ::_thesis: x in { (card B) where B is Basis of (M | X1) : verum }
then consider B1 being Basis of X such that
A5: x = card B1 ;
reconsider B2 = B1 as Basis of (M | X1) by A3, YELLOW12:32;
x = card B2 by A5;
hence x in { (card B) where B is Basis of (M | X1) : verum } ; ::_thesis: verum
end;
assume x in { (card B) where B is Basis of (M | X1) : verum } ; ::_thesis: x in { (card B) where B is Basis of X : verum }
then consider B1 being Basis of (M | X1) such that
A6: x = card B1 ;
reconsider B2 = B1 as Basis of X by A3, YELLOW12:32;
x = card B2 by A6;
hence x in { (card B) where B is Basis of X : verum } ; ::_thesis: verum
end;
weight X = weight (M | X1) by A4, TARSKI:1;
then weight X c= omega by WAYBEL23:def_6;
then A7: X is second-countable by WAYBEL23:def_6;
for p being Point of X ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic
proof
let p be Point of X; ::_thesis: ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic
p in the carrier of X ;
then reconsider p1 = p as Point of M by A2;
consider U1 being a_neighborhood of p1, S1 being open Subset of (TOP-REAL n) such that
A8: U1,S1 are_homeomorphic by Def4;
consider U2 being open Subset of M, S2 being open Subset of (TOP-REAL n) such that
A9: ( U2 c= U1 & p1 in U2 & U2,S2 are_homeomorphic ) by A8, Th11;
reconsider X2 = X as non empty open SubSpace of M by A1;
reconsider U = U2 /\ X1 as Subset of X2 by XBOOLE_1:17;
A10: M | U2,(TOP-REAL n) | S2 are_homeomorphic by A9, METRIZTS:def_1;
then consider f being Function of (M | U2),((TOP-REAL n) | S2) such that
A11: f is being_homeomorphism by T_0TOPSP:def_1;
A12: p in U2 /\ X1 by A9, XBOOLE_0:def_4;
U is open by TSEP_1:17;
then reconsider U = U as a_neighborhood of p by A12, CONNSP_2:3;
U c= U2 by XBOOLE_1:17;
then U c= [#] (M | U2) by PRE_TOPC:def_5;
then reconsider U3 = U as Subset of (M | U2) ;
U3,f .: U3 are_homeomorphic by A11, METRIZTS:3;
then A13: (M | U2) | U3,((TOP-REAL n) | S2) | (f .: U3) are_homeomorphic by METRIZTS:def_1;
reconsider M2 = M | U2 as non empty SubSpace of M by A9;
reconsider T2 = (TOP-REAL n) | S2 as non empty SubSpace of TOP-REAL n by A10, A9, YELLOW14:18;
reconsider f2 = f as Function of M2,T2 ;
A14: for P being Subset of M2 holds
( P is open iff f2 .: P is open ) by A11, TOPGRP_1:25;
f .: U3 c= [#] ((TOP-REAL n) | S2) ;
then A15: f .: U3 c= S2 by PRE_TOPC:def_5;
A16: X1 in the topology of M by PRE_TOPC:def_2;
U2 = [#] M2 by PRE_TOPC:def_5;
then U3 in the topology of M2 by A16, PRE_TOPC:def_4;
then U3 is open by PRE_TOPC:def_2;
then reconsider S = f .: U3 as open Subset of T2 by A14;
S in the topology of T2 by PRE_TOPC:def_2;
then consider Q being Subset of (TOP-REAL n) such that
A17: ( Q in the topology of (TOP-REAL n) & S = Q /\ ([#] T2) ) by PRE_TOPC:def_4;
A18: [#] T2 = S2 by PRE_TOPC:def_5;
S2 in the topology of (TOP-REAL n) by PRE_TOPC:def_2;
then S in the topology of (TOP-REAL n) by A18, A17, PRE_TOPC:def_1;
then reconsider S = S as open Subset of (TOP-REAL n) by PRE_TOPC:def_2;
take U ; ::_thesis: ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic
take S ; ::_thesis: U,S are_homeomorphic
U c= X1 ;
then U c= [#] (M | X1) by PRE_TOPC:def_5;
then reconsider U4 = U as Subset of (M | X1) ;
reconsider U5 = U as Subset of M ;
A19: (M | X1) | U4 = M | U5 by GOBOARD9:2;
(M | U2) | U3 = M | U5 by GOBOARD9:2;
then A20: TopStruct(# the carrier of (X | U), the topology of (X | U) #) = TopStruct(# the carrier of ((M | U2) | U3), the topology of ((M | U2) | U3) #) by A19, A3, PRE_TOPC:36;
((TOP-REAL n) | S2) | (f .: U3) = (TOP-REAL n) | S by A15, PRE_TOPC:7;
hence U,S are_homeomorphic by A13, A20, METRIZTS:def_1; ::_thesis: verum
end;
then X is n -locally_euclidean by Def4;
hence X is n -manifold by A7; ::_thesis: verum
end;
end;
registration
cluster non empty TopSpace-like manifold-like for TopStruct ;
existence
ex b1 being non empty TopSpace st b1 is manifold-like
proof
take TOP-REAL 0 ; ::_thesis: TOP-REAL 0 is manifold-like
thus TOP-REAL 0 is manifold-like ; ::_thesis: verum
end;
end;
definition
mode manifold is non empty manifold-like TopSpace;
end;