:: The Definition of Topological Manifolds
:: by Marco Riccardi
::
:: Received August 17, 2010
:: Copyright (c) 2010 Association of Mizar Users
environ
vocabularies NUMBERS, SUBSET_1, XREAL_0, ORDINAL1, PRE_TOPC, EUCLID, ARYTM_1,
ARYTM_3, SUPINF_2, XBOOLE_0, FUNCOP_1, ORDINAL2, TOPS_1, RCOMP_1,
XXREAL_0, METRIC_1, TARSKI, STRUCT_0, REAL_1, COMPLEX1, SETFAM_1,
PCOMPS_1, TOPS_2, T_0TOPSP, CONNSP_2, FUNCT_1, RELAT_1, CARD_1, SQUARE_1,
TOPMETR, MEMBERED, XXREAL_1, XXREAL_2, WAYBEL23, COMPTS_1, RLVECT_3,
NATTRA_1, ZFMISC_1, FRECHET, CARD_3, MFOLD_1;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, FUNCT_1, TOPS_2, RELAT_1,
RELSET_1, PARTFUN1, FUNCT_2, ORDINAL1, NAT_1, NUMBERS, VALUED_0,
VALUED_1, XCMPLX_0, XREAL_0, XXREAL_0, COMPLEX1, REAL_1, STRUCT_0,
RVSUM_1, PRE_TOPC, METRIC_1, TOPREAL9, TOPS_1, ALGSTR_0, RLVECT_1,
BORSUK_3, CONNSP_2, TSEP_1, METRIZTS, PCOMPS_1, COMPTS_1, EUCLID,
SQUARE_1, TOPMETR, TMAP_1, XXREAL_1, MEMBERED, XXREAL_2, TOPREAL6,
WAYBEL23, CANTOR_1, CARD_1, TDLAT_3, ZFMISC_1, CARD_3, YELLOW_8, FRECHET;
constructors MONOID_0, TOPREAL9, TOPREALB, SQUARE_1, FUNCSDOM, TOPS_1, TSEP_1,
BORSUK_3, METRIZTS, PCOMPS_1, RLVECT_1, COMPLEX1, COMPTS_1, XCMPLX_0,
NAT_1, EUCLID, BINOP_2, TOPMETR, TMAP_1, MEMBERED, XXREAL_2, TOPREAL6,
SEQ_1, WAYBEL23, CANTOR_1, TDLAT_3, FUNCT_2, YELLOW_8, FRECHET;
registrations XBOOLE_0, XXREAL_0, XREAL_0, XCMPLX_0, SQUARE_1, NAT_1,
MEMBERED, STRUCT_0, METRIC_1, MONOID_0, EUCLID, TOPALG_2, VALUED_0,
FINSEQ_1, FUNCT_1, RELAT_1, PRE_TOPC, TOPS_1, CARD_1, TSEP_1, TOPREAL9,
PCOMPS_1, RLVECT_1, COMPLEX1, TMAP_1, COMPTS_1, TOPMETR, XXREAL_2,
TOPREAL6, SPPOL_1, WAYBEL23, METRIZTS, RLVECT_3, TOPREAL1, YELLOW13,
YELLOW_8, KURATO_2, SUBSET_1;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, XREAL_0, XXREAL_2, XCMPLX_0, ALGSTR_0, STRUCT_0,
RELAT_1, FUNCT_1, FUNCT_2, ORDINAL1, MEMBERED, PRE_TOPC, TOPS_2,
T_0TOPSP, EUCLID, PCOMPS_1, TOPREAL9, SQUARE_1, ABSVALUE, TMAP_1,
METRIZTS, FRECHET, YELLOW_8, WAYBEL23;
theorems TOPRNS_1, XREAL_0, TARSKI, FUNCT_2, EUCLID, XBOOLE_1, FUNCOP_1,
JORDAN2C, XCMPLX_1, ABSVALUE, XXREAL_1, XXREAL_2, GOBOARD6, XREAL_1,
RLVECT_1, ORDINAL1, ZFMISC_1, SETFAM_1, PRE_TOPC, TOPS_1, CONNSP_2,
METRIZTS, PCOMPS_1, T_0TOPSP, YELLOW14, TOPGRP_1, XBOOLE_0, TSEP_1,
BORSUK_3, TOPREAL9, BORSUK_4, RELAT_1, FUNCT_1, TOPALG_1, TOPS_2,
JGRAPH_1, RELSET_1, SQUARE_1, EUCLID_2, XXREAL_0, JGRAPH_2, TOPMETR,
TOPREAL3, JORDAN6, GOBOARD9, RCOMP_1, JORDAN, WAYBEL23, YELLOW12,
MEMBERED, JGRAPH_3, JGRAPH_5, TDLAT_3, FRECHET, CARD_3, YELLOW_8;
schemes FUNCT_2, TREES_2;
begin :: Preliminaries
registration
let x, y be set;
cluster {[x,y]} -> one-to-one;
correctness
proof
set f = {[x,y]};
let x1, x2 be set;
assume x1 in dom f & x2 in dom f & f.x1 = f.x2; then
A1: x1 in {x} & x2 in {x} by RELAT_1:23;
hence x1 = x by TARSKI:def 1 .= x2 by A1,TARSKI:def 1;
end;
end;
reserve n for natural number;
theorem Th1:
for T being non empty TopSpace holds T , T | [#]T are_homeomorphic
proof
let X be non empty TopSpace;
set f = id X;
A1: dom f = [#]X by RELAT_1:71;
A2: [#](X | ([#]X))=the carrier of (the TopStruct of X) by TSEP_1:100
.= [#]X;
then A3: rng f = [#](X | ([#]X)) by RELAT_1:71;
reconsider f 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;
assume P is closed; then
([#]X) \ P is open by PRE_TOPC:def 6; then
A4: ([#]X) \ P in the topology of X by PRE_TOPC:def 5;
A5: for x being set holds x in (f")"P iff x in P
proof
let x be set;
hereby
assume A6: x in (f")"P;
x in f.:P by A6,A3,TOPS_2:67; then
consider y be 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;
end;
assume A8: x in 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:67;
end;
A9: ([#]X) \ P = ([#] (X | ([#]X))) \ (f")"P by A2,A5,TARSKI:2;
([#]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 9; then
([#] (X | ([#]X))) \ (f")"P is open by A9,PRE_TOPC:def 5;
hence (f")"P is closed by PRE_TOPC:def 6;
end; then
A10: f" is continuous by PRE_TOPC:def 12;
f is continuous by JGRAPH_1:63; then
f is being_homeomorphism by A1,A3,A10,TOPS_2:def 5;
hence thesis by T_0TOPSP:def 1;
end;
theorem Th2:
for X being non empty SubSpace of TOP-REAL n, f being Function of X,R^1
st f is continuous
ex g being Function of X,TOP-REAL n st
(for a being Point of X, b being Point of TOP-REAL n, r being real number
st a = b & f.a = r holds g.b = r*b) & g is continuous
proof
let X be non empty SubSpace of TOP-REAL n, f be Function of X,R^1;
assume A1: f is continuous;
defpred P[set,set] means
for b being Point of TOP-REAL n, 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 P[x,y]
proof
let x be Element of X;
reconsider r = f.x as Real by TOPMETR:24;
A3: x in the carrier of X;
[#] X c= [#] TOP-REAL n by PRE_TOPC:def 9; then
reconsider p = x as Point of TOP-REAL n by A3;
set y = r*p;
take y;
thus P[x,y];
end;
ex g being Function of the carrier of X, the carrier of TOP-REAL n
st for x being Element of X holds P[x,g.x] from FUNCT_2:sch 3(A2); then
consider g be Function of X, TOP-REAL n such that
A4: for x being Element of X holds for b being Point of TOP-REAL n,
r being real number st x = b & f.x = r holds g.x = r*b;
take g;
for p being Point of X, 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, V be Subset of TOP-REAL n;
A5: n in NAT by ORDINAL1:def 13;
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
reconsider gp = g.p as Point of Euclid n by TOPREAL3:13;
A6: p in the carrier of X;
[#] X c= [#] TOP-REAL n by PRE_TOPC:def 9; then
reconsider pp = p as Point of TOP-REAL n1 by A6;
reconsider fp = f.p as real number;
assume g.p in V & V is open; then
g.p in Int V by TOPS_1:55; then
consider r0 be real number such that
A7: r0 > 0 and
A8: Ball(gp,r0) c= V by A5,GOBOARD6:8;
per cases;
suppose A9: fp = 0;
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 5; then
W2 in the topology of X by PRE_TOPC:def 9; then
A10: W2 is open by PRE_TOPC:def 5;
p in Ball(pp, r0/2) by A7,JORDAN:16; then
A11: p in W2 by XBOOLE_0:def 4;
set WW2 = {|.p2.| where p2 is Point of TOP-REAL n: p2 in W2};
A12: |.pp.| in WW2 by A11;
for x being set st x in WW2 holds x is real
proof
let x be set;
assume x in WW2; then
consider p2 be Point of TOP-REAL n1 such that
A13: x = |.p2.| & p2 in W2;
thus x is real by A13;
end; then
reconsider WW2 as non empty real-membered set by A12,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;
assume x in WW2; then
consider p2 be Point of TOP-REAL n1 such that
A14: x = |.p2.| & p2 in W2;
p2 in Ball(pp, r0/2) by A14,XBOOLE_0:def 4; then
A15: |. p2 - pp .| < r0/2 by TOPREAL9:7;
|.p2.| - |. -pp .| <= |. p2 + -pp .| by TOPRNS_1:32; then
|.p2.| - |. pp .| <= |. p2 + -pp .| by TOPRNS_1:27; then
|.p2.| - |.pp.| <= r0/2 by A15,XXREAL_0:2; then
|.p2.| - |.pp.| + |.pp.| <= r0/2 + |.pp.| by XREAL_1:8;
hence x <= |.pp.|+r0/2 by A14;
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;
A16: m >= 0
proof
assume A17: m < 0;
A18: m is UpperBound of WW2 by XXREAL_2:def 3;
|.pp.| in WW2 by A11;
hence contradiction by A17,A18,XXREAL_2:def 1;
end;
per cases by A16;
suppose A19: m = 0;
set G1 = REAL;
REAL in the topology of R^1 by PRE_TOPC:def 1,TOPMETR:24; then
reconsider G1 as open Subset of R^1 by PRE_TOPC:def 5;
fp in G1 by XREAL_0:def 1; then
consider W1 be Subset of X such that
A20: p in W1 and
A21: W1 is open and
f.:W1 c= G1 by A1,JGRAPH_2:20;
reconsider W3 = W1 /\ W2 as Subset of X;
take W3;
thus p in W3 by A20,A11,XBOOLE_0:def 4;
thus W3 is open by A21,A10;
g.:W3 c= Ball(gp,r0)
proof
let x be set;
assume x in g.:W3; then
consider q be set such that
A22: q in dom g and
A23: q in W3 and
A24: g.q = x by FUNCT_1:def 12;
reconsider q as Point of X by A22;
A25: q in the carrier of X;
[#] X c= [#] TOP-REAL n by PRE_TOPC:def 9; then
reconsider qq = q as Point of TOP-REAL n1 by A25;
reconsider fq = f.q as real number;
A26: x = fq * qq by A4,A24; then
reconsider gq = x as Point of Euclid n by TOPREAL3:13;
reconsider gpp = gp as Point of TOP-REAL n1;
reconsider gqq = gq as Point of TOP-REAL n1 by A26;
A27: gpp = fp * pp by A4;
reconsider r2 = fq-fp as Real by XREAL_0:def 1;
A28: abs(fq-fp)*|.qq.| = abs(r2)*|.qq.| .= |.(fq-fp)*qq.|
by TOPRNS_1:8;
qq in W2 by A23,XBOOLE_0:def 4; then
|.qq.| in WW2; then
A29: |.qq.| <= m by XXREAL_2:4;
A30: gpp = 0.TOP-REAL n1 by A27,A9,EUCLID:33;
|. gqq + -gpp .| <= |. gqq .| + |. -gpp .| by EUCLID_2:74; then
|. gqq + -gpp .| <= |. gqq .| + |. 0.TOP-REAL n1 .|
by JGRAPH_5:13,A30; then
|. gqq + -gpp .| <= |. gqq .| + 0 by EUCLID_2:61; then
|. gqq - gpp .| < r0 by A4,A24,A9,A29,A28,A7,A19; then
gqq in Ball(gpp,r0);
hence x in Ball(gp,r0) by TOPREAL9:13;
end;
hence thesis by A8,XBOOLE_1:1;
end;
suppose A31: m > 0;
set G1 = ]. fp-r0/m, fp+r0/m .[;
reconsider G1 as open Subset of R^1
by JORDAN6:46,TOPMETR:24,XXREAL_1:225;
A32: 0 + fp < r0/m + fp by A31,A7,XREAL_1:8;
-r0/m + fp < 0 + fp by A31,A7,XREAL_1:8; then
fp in G1 by A32,XXREAL_1:4; then
consider W1 be Subset of X such that
A33: p in W1 and
A34: W1 is open and
A35: f.:W1 c= G1 by A1,JGRAPH_2:20;
reconsider W3 = W1 /\ W2 as Subset of X;
take W3;
thus p in W3 by A33,A11,XBOOLE_0:def 4;
thus W3 is open by A34,A10;
g.:W3 c= Ball(gp,r0)
proof
let x be set;
assume x in g.:W3; then
consider q be set such that
A36: q in dom g and
A37: q in W3 and
A38: g.q = x by FUNCT_1:def 12;
reconsider q as Point of X by A36;
A39: q in the carrier of X;
[#] X c= [#] TOP-REAL n by PRE_TOPC:def 9; then
reconsider qq = q as Point of TOP-REAL n1 by A39;
reconsider fq = f.q as real number;
A40: x = fq * qq by A4,A38; then
reconsider gq = x as Point of Euclid n by TOPREAL3:13;
reconsider gpp = gp as Point of TOP-REAL n1;
reconsider gqq = gq as Point of TOP-REAL n1 by A40;
A41: gpp = fp * pp by A4;
reconsider r2 = fq as Real by XREAL_0:def 1;
A42: abs(fq)*|.qq.| = abs(r2)*|.qq.| .= |.fq*qq.|
by TOPRNS_1:8;
A43: q in dom f by A39,FUNCT_2:def 1;
q in W1 by A37,XBOOLE_0:def 4; then
f.q in f.:W1 by A43,FUNCT_1:def 12; then
abs(fq-fp) < r0/m by A35,RCOMP_1:8; then
abs(fq)*m < r0/m*m by A9,A31,XREAL_1:70; then
abs(fq)*m < r0/(m/m) by XCMPLX_1:83; then
A44: abs(fq)*m < r0/1 by A31,XCMPLX_1:60;
qq in W2 by A37,XBOOLE_0:def 4; then
|.qq.| in WW2; then
|.qq.| <= m by XXREAL_2:4; then
A45: |.qq.|*abs(fq) <= m*abs(fq) by XREAL_1:66;
A46: gpp = 0.TOP-REAL n1 by A41,A9,EUCLID:33;
A47: |. gqq .| < r0 by A40,A45,A42,A44,XXREAL_0:2;
|. gqq + -gpp .| <= |. gqq .| + |. -gpp .| by EUCLID_2:74; then
|. gqq + -gpp .| <= |. gqq .| + |. 0.TOP-REAL n1 .|
by JGRAPH_5:13,A46; then
|. gqq + -gpp .| <= |. gqq .| + 0 by EUCLID_2:61; then
|. gqq - gpp .| < r0 by A47,XXREAL_0:2; then
gqq in Ball(gpp,r0);
hence x in Ball(gp,r0) by TOPREAL9:13;
end;
hence thesis by A8,XBOOLE_1:1;
end;
end;
suppose A48: fp <> 0;
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 5; then
W2 in the topology of X by PRE_TOPC:def 9; then
A49: W2 is open by PRE_TOPC:def 5;
p in Ball(pp, r0/2/abs(fp)) by JORDAN:16,A48,A7; then
A50: p in W2 by XBOOLE_0:def 4;
set WW2 = {|.p2.| where p2 is Point of TOP-REAL n: p2 in W2};
A51: |.pp.| in WW2 by A50;
for x being set st x in WW2 holds x is real
proof
let x be set;
assume x in WW2; then
consider p2 be Point of TOP-REAL n1 such that
A52: x = |.p2.| & p2 in W2;
thus x is real by A52;
end; then
reconsider WW2 as non empty real-membered set by A51,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;
assume x in WW2; then
consider p2 be Point of TOP-REAL n1 such that
A53: x = |.p2.| & p2 in W2;
p2 in Ball(pp, r0/2/abs(fp)) by A53,XBOOLE_0:def 4; then
A54: |. p2 - pp .| < r0/2/abs(fp) by TOPREAL9:7;
|.p2.| - |. -pp .| <= |. p2 + -pp .| by TOPRNS_1:32; then
|.p2.| - |. pp .| <= |. p2 + -pp .| by TOPRNS_1:27; then
|.p2.| - |.pp.| <= r0/2/abs(fp) by A54,XXREAL_0:2; then
|.p2.| - |.pp.| + |.pp.| <= r0/2/abs(fp) + |.pp.| by XREAL_1:8;
hence x <= |.pp.|+r0/2/abs(fp) by A53;
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;
A55: m >= 0
proof
assume A56: m < 0;
A57: m is UpperBound of WW2 by XXREAL_2:def 3;
|.pp.| in WW2 by A50;
hence contradiction by A56,A57,XXREAL_2:def 1;
end;
per cases by A55;
suppose A58: m = 0;
set G1 = REAL;
REAL in the topology of R^1 by PRE_TOPC:def 1,TOPMETR:24; then
reconsider G1 as open Subset of R^1 by PRE_TOPC:def 5;
fp in G1 by XREAL_0:def 1; then
consider W1 be Subset of X such that
A59: p in W1 and
A60: W1 is open and
f.:W1 c= G1 by A1,JGRAPH_2:20;
reconsider W3 = W1 /\ W2 as Subset of X;
take W3;
thus p in W3 by A59,A50,XBOOLE_0:def 4;
thus W3 is open by A60,A49;
g.:W3 c= Ball(gp,r0)
proof
let x be set;
assume x in g.:W3; then
consider q be set such that
A61: q in dom g and
A62: q in W3 and
A63: g.q = x by FUNCT_1:def 12;
reconsider q as Point of X by A61;
A64: q in the carrier of X;
[#] X c= [#] TOP-REAL n by PRE_TOPC:def 9; then
reconsider qq = q as Point of TOP-REAL n1 by A64;
reconsider fq = f.q as real number;
A65: x = fq * qq by A4,A63; then
reconsider gq = x as Point of Euclid n by TOPREAL3:13;
reconsider gpp = gp as Point of TOP-REAL n1;
reconsider gqq = gq as Point of TOP-REAL n1 by A65;
A66: 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;
A67: abs(fq-fp)*|.qq.| = abs(r2)*|.qq.| .= |.(fq-fp)*qq.|
by TOPRNS_1:8;
qq in W2 by A62,XBOOLE_0:def 4; then
|.qq.| in WW2; then
A68: |.qq.| <= m by XXREAL_2:4;
A69: abs(fp)*|.qq-pp.| = abs(r3)*|.qq-pp.| .= |.fp*(qq-pp).|
by TOPRNS_1:8;
qq in W2 by A62,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 A48,XREAL_1:70; then
abs(fp)*|.qq-pp.| < r0/2/(abs(fp)/abs(fp)) by XCMPLX_1:82; then
A70: abs(fp)*|.qq-pp.| < r0/2/1 by A48,XCMPLX_1:60;
A71: |.(fq-fp)*qq.| + |.fp*(qq-pp).| < r0/2+r0/2
by A68,A70,A69,A67,A58,XREAL_1:10;
|.(fq-fp)*qq + fp*(qq-pp).| <= |.(fq-fp)*qq.| + |.fp*(qq-pp).|
by EUCLID_2:74; then
A72: |.(fq-fp)*qq + fp*(qq-pp).| < r0 by A71,XXREAL_0:2;
(fq-fp)*qq + fp*(qq-pp) = fq*qq -fp*qq + fp*(qq-pp) by EUCLID:54
.= fq*qq -fp*qq + (fp*qq -fp*pp) by EUCLID:53
.= fq*qq -fp*qq +fp*qq -fp*pp by EUCLID:49
.= fq*qq - fp*pp by EUCLID:52; then
gqq in Ball(gpp,r0) by A65,A72,A66;
hence x in Ball(gp,r0) by TOPREAL9:13;
end;
hence thesis by A8,XBOOLE_1:1;
end;
suppose A73: m > 0;
set G1 = ]. fp-r0/2/m, fp+r0/2/m .[;
reconsider G1 as open Subset of R^1
by JORDAN6:46,TOPMETR:24,XXREAL_1:225;
A74: 0 + fp < r0/2/m + fp by A73,A7,XREAL_1:8;
-r0/2/m + fp < 0 + fp by A73,A7,XREAL_1:8; then
fp in G1 by A74,XXREAL_1:4; then
consider W1 be Subset of X such that
A75: p in W1 and
A76: W1 is open and
A77: f.:W1 c= G1 by A1,JGRAPH_2:20;
reconsider W3 = W1 /\ W2 as Subset of X;
take W3;
thus p in W3 by A75,A50,XBOOLE_0:def 4;
thus W3 is open by A76,A49;
g.:W3 c= Ball(gp,r0)
proof
let x be set;
assume x in g.:W3; then
consider q be set such that
A78: q in dom g and
A79: q in W3 and
A80: g.q = x by FUNCT_1:def 12;
reconsider q as Point of X by A78;
A81: q in the carrier of X;
[#] X c= [#] TOP-REAL n by PRE_TOPC:def 9; then
reconsider qq = q as Point of TOP-REAL n1 by A81;
reconsider fq = f.q as real number;
A82: x = fq * qq by A4,A80; then
reconsider gq = x as Point of Euclid n by TOPREAL3:13;
reconsider gpp = gp as Point of TOP-REAL n1;
reconsider gqq = gq as Point of TOP-REAL n1 by A82;
A83: 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;
A84: abs(fq-fp)*|.qq.| = abs(r2)*|.qq.|
.= |.(fq-fp)*qq.| by TOPRNS_1:8;
A85: q in dom f by A81,FUNCT_2:def 1;
q in W1 by A79,XBOOLE_0:def 4; then
f.q in f.:W1 by A85,FUNCT_1:def 12; then
abs(fq-fp) < r0/2/m by A77,RCOMP_1:8; then
abs(fq-fp)*m < r0/2/m*m by A73,XREAL_1:70; then
abs(fq-fp)*m < r0/2/(m/m) by XCMPLX_1:83; then
A86: abs(fq-fp)*m < r0/2/1 by A73,XCMPLX_1:60;
qq in W2 by A79,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:66; then
A87: |.(fq-fp)*qq.| < r0/2 by A84,A86,XXREAL_0:2;
A88: abs(fp)*|.qq-pp.| = abs(r3)*|.qq-pp.| .= |.fp*(qq-pp).|
by TOPRNS_1:8;
qq in W2 by A79,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 A48,XREAL_1:70; then
abs(fp)*|.qq-pp.| < r0/2/(abs(fp)/abs(fp)) by XCMPLX_1:82; then
A89: abs(fp)*|.qq-pp.| < r0/2/1 by A48,XCMPLX_1:60;
A90: |.(fq-fp)*qq.| + |.fp*(qq-pp).| < r0/2+r0/2
by A87,A89,A88,XREAL_1:10;
|.(fq-fp)*qq + fp*(qq-pp).| <= |.(fq-fp)*qq.| + |.fp*(qq-pp).|
by EUCLID_2:74; then
A91: |.(fq-fp)*qq + fp*(qq-pp).| < r0 by A90,XXREAL_0:2;
(fq-fp)*qq + fp*(qq-pp) = fq*qq -fp*qq + fp*(qq-pp) by EUCLID:54
.= fq*qq -fp*qq + (fp*qq -fp*pp) by EUCLID:53
.= fq*qq -fp*qq +fp*qq -fp*pp by EUCLID:49
.= fq*qq - fp*pp by EUCLID:52; then
gqq in Ball(gpp,r0) by A82,A83,A91;
hence x in Ball(gp,r0) by TOPREAL9:13;
end;
hence thesis by A8,XBOOLE_1:1;
end;
end;
end;
hence thesis by A4,JGRAPH_2:20;
end;
definition
let n;
let S be Subset of TOP-REAL n;
attr S is ball means :Def1:
ex p being Point of TOP-REAL n, r being real number st S = Ball(p,r);
end;
registration
let n;
cluster ball Subset of TOP-REAL n;
correctness
proof
take Ball(the Point of TOP-REAL n,the real number);
thus thesis by Def1;
end;
cluster ball -> open Subset of TOP-REAL n;
correctness
proof
let S be Subset of TOP-REAL n;
assume S is ball; then
ex p be Point of TOP-REAL n, r be real number st S = Ball(p,r) by Def1;
hence thesis;
end;
end;
registration
let n;
cluster non empty ball Subset of TOP-REAL n;
correctness
proof
reconsider S = Ball(0.(TOP-REAL n),1) as ball Subset of TOP-REAL n by Def1;
take S;
thus thesis;
end;
end;
reserve p for Point of TOP-REAL n, r for real number;
theorem Th3:
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 S be open Subset of TOP-REAL n;
assume A1: p in S;
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 5;
reconsider x=p as Element of Euclid n by A2;
consider r be Real such that
A4: r > 0 & Ball(x,r) c= S by A1,A3,PCOMPS_1:def 5;
reconsider r as positive (real number) by A4;
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
reconsider B = Ball(p,r) as ball Subset of TOP-REAL n by Def1;
take B;
reconsider p1=p as Point of TOP-REAL n1;
Ball(x,r) = Ball(p1,r) by TOPREAL9:13;
hence thesis by A4,GOBOARD6:4;
end;
definition
let n,p,r;
func Tball(p,r) -> SubSpace of TOP-REAL n equals
(TOP-REAL n) | Ball(p,r);
correctness;
end;
definition
let n;
func Tunit_ball(n) -> SubSpace of TOP-REAL n equals
Tball(0.(TOP-REAL n),1);
correctness;
end;
registration
let n;
cluster Tunit_ball(n) -> non empty;
correctness;
let p;
let s be positive (real number);
cluster Tball(p,s) -> non empty;
correctness;
end;
theorem Th4:
the carrier of Tball(p,r) = Ball(p,r)
proof
[#]Tball(p,r) = Ball(p,r) by PRE_TOPC:def 10;
hence thesis;
end;
theorem Th5:
n <> 0 & p is Point of Tunit_ball(n) implies |. p .| < 1
proof
reconsider j = 1 as real number;
assume n <> 0; then
reconsider n1 = n as non empty Element of NAT by ORDINAL1:def 13;
assume p is Point of Tunit_ball(n); then
p in the carrier of Tball(0.(TOP-REAL n1),j);
then p in Ball(0.(TOP-REAL n1),1) by Th4;
hence thesis by TOPREAL9:10;
end;
theorem Th6:
for f being Function of Tunit_ball n, TOP-REAL n st n <> 0 &
for a being Point of Tunit_ball n, 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 f being Function of Tunit_ball n, TOP-REAL n such that
A1: n <> 0 and
A2: for a being Point of Tunit_ball n, b being Point of TOP-REAL n st
a = b holds f.a = 1/(1-|.b.|*|.b.|)*b;
A3: dom f = [#]Tunit_ball n by FUNCT_2:def 1;
A4: [#] Tunit_ball n c= [#] TOP-REAL n by PRE_TOPC:def 9;
reconsider n1 = n as non empty Element of NAT by A1,ORDINAL1:def 13;
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;
assume y in [#]TOP-REAL n1; then
reconsider py = y as Point of TOP-REAL n1;
per cases;
suppose A5: |.py.| = 0;
set x = py;
|.x - 0.TOP-REAL n1.| < 1 by A5,RLVECT_1:26; then
x in Ball(0.TOP-REAL n, 1); then
A6: x in dom f by A3,Th4;
take x;
f.x = 1/(1-|.x.|*|.x.|)*x by A6,A2
.= py by A5,EUCLID:33;
hence [x,y] in f by A6,FUNCT_1:def 4;
end;
suppose A7: |.py.| <> 0;
set p2 = |.py.|*|.py.|;
set x = 2/(1+sqrt(1+4*p2))*py;
reconsider r = 2/(1+sqrt(1+4*p2)) as Real;
A8: sqrt(1+4*p2) >= 0 by SQUARE_1:def 4;
A9: |.x.| = abs(r)*|.py.| by TOPRNS_1:8
.= r*|.py.| by A8,ABSVALUE:def 1;
|.x.| < 1
proof
|.py.|*4 + (1+4*p2) > 0 + (1+4*p2) by A7,XREAL_1:8; then
sqrt((1+2*|.py.|)^2) > sqrt(1+4*p2) by SQUARE_1:95; then
1+2*|.py.| > sqrt(1+4*p2) by SQUARE_1:89; then
1+2*|.py.|-sqrt(1+4*p2) > sqrt(1+4*p2)-sqrt(1+4*p2) by XREAL_1:11; then
1-sqrt(1+4*p2)+2*|.py.|-2*|.py.| > 0 - 2*|.py.| by XREAL_1:11; then
(1-sqrt(1+4*p2))*1 > -2*|.py.|; then
(1-sqrt(1+4*p2))*((1+sqrt(1+4*p2))/(1+sqrt(1+4*p2))) > -2*|.py.|
by A8,XCMPLX_1:60; then
(1-(sqrt(1+4*p2))^2)/(1+sqrt(1+4*p2)) > -2*|.py.|; then
(1-(1+4*p2))/(1+sqrt(1+4*p2)) > -2*|.py.| by SQUARE_1:def 4; then
-4*p2/(1+sqrt(1+4*p2)) > -2*|.py.|; then
2*|.py.|*(2*|.py.|)/(1+sqrt(1+4*p2))
< 2*|.py.| by XREAL_1:26; then
(2*|.py.|)*((2*|.py.|)/(1+sqrt(1+4*p2)))/(2*|.py.|)
< 2*|.py.|/(2*|.py.|) by A7,XREAL_1:76; then
(2*|.py.|)*((2*|.py.|)/(1+sqrt(1+4*p2)))/(2*|.py.|) < 1
by A7,XCMPLX_1:60; then
((2*|.py.|)/(1+sqrt(1+4*p2)))/((2*|.py.|)/(2*|.py.|)) < 1
by XCMPLX_1:78; then
((2*|.py.|)/(1+sqrt(1+4*p2)))/1 < 1 by A7,XCMPLX_1:60;
hence thesis by A9;
end; then
|.x - 0.TOP-REAL n1.| < 1 by RLVECT_1:26; then
x in Ball(0.TOP-REAL n1, 1); then
A10: x in dom f by A3,Th4;
take x;
A11: sqrt(1+4*p2)>=0 by SQUARE_1:def 4;
A12: 1-sqrt(1+4*p2)<>0
proof
assume 1-sqrt(1+4*p2)=0; then
(sqrt(1+4*p2))^2 = 1; then
1+4*p2 = 1 by SQUARE_1:def 4;
hence contradiction by A7;
end;
|.x.|*|.x.| = (2/(1+sqrt(1+4*p2)))*(2/(1+sqrt(1+4*p2)))*p2 by A9
.= (2*2)/((1+sqrt(1+4*p2))*(1+sqrt(1+4*p2)))*p2 by XCMPLX_1:77
.= 4/(1+2*sqrt(1+4*p2)+(sqrt(1+4*p2))^2)*p2
.= 4/(1+2*sqrt(1+4*p2)+(1+4*p2))*p2 by SQUARE_1:def 4
.= 4/(2*(1+sqrt(1+4*p2)+2*p2))*p2
.= 4/2/(1+sqrt(1+4*p2)+2*p2)*p2 by XCMPLX_1:79
.= (2*p2)/(1+2*p2+sqrt(1+4*p2)); then
A13: 1-|.x.|*|.x.| = (1+2*p2+sqrt(1+4*p2))/(1+2*p2+sqrt(1+4*p2))
+ -(2*p2)/(1+2*p2+sqrt(1+4*p2)) by A11,XCMPLX_1:60
.= (1+sqrt(1+4*p2))/(1+2*p2+sqrt(1+4*p2))*1
.= ((1+sqrt(1+4*p2))/(1+2*p2+sqrt(1+4*p2)))*
((1-sqrt(1+4*p2))/(1-sqrt(1+4*p2))) by A12,XCMPLX_1:60
.= ((1+sqrt(1+4*p2))*(1-sqrt(1+4*p2)))/
((1-sqrt(1+4*p2))*(1+2*p2+sqrt(1+4*p2))) by XCMPLX_1:77
.= (1-(sqrt(1+4*p2))^2)/
(1+2*p2-2*p2*sqrt(1+4*p2)-sqrt(1+4*p2)*sqrt(1+4*p2))
.= (1-(1+4*p2))/
(1+2*p2-2*p2*sqrt(1+4*p2)-(sqrt(1+4*p2))^2) by SQUARE_1:def 4
.= (-4*p2)/(1+2*p2-2*p2*sqrt(1+4*p2)-(1+4*p2)) by SQUARE_1:def 4
.= (-4*p2)/((-2*p2)*(1+sqrt(1+4*p2)))
.= 2*(-2*p2)/(-2*p2)/(1+sqrt(1+4*p2)) by XCMPLX_1:79
.= 2*((-2*p2)/(-2*p2))/(1+sqrt(1+4*p2))
.= 2*1/(1+sqrt(1+4*p2)) by A7,XCMPLX_1:60
.= 2/(1+sqrt(1+4*p2));
f.x = 1/(1-|.x.|*|.x.|)*x by A2,A10
.= (r/r)*py by A13,EUCLID:34
.= 1*py by A8,XCMPLX_1:60
.= py by EUCLID:33;
hence [x,y] in f by A10,FUNCT_1:def 4;
end;
end; then
A14: rng f = [#]TOP-REAL n1 by RELSET_1:23;
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;
A15: [#]Tunit_ball n c= [#] TOP-REAL n by PRE_TOPC:def 9;
assume A16: x1 in dom f; 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; 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;
A20: 1/(1-|.px1.|*|.px1.|)*px1 = f.x2 by A19,A16,A2
.= 1/(1-|.px2.|*|.px2.|)*px2 by A17,A2;
per cases;
suppose A21: |.px1.| = 0; then
A22: px1 = 0.TOP-REAL n by EUCLID_2:64;
per cases by A22,EUCLID:35,A20,EUCLID:32;
suppose 1/(1-|.px2.|*|.px2.|) = 0; then
1-|.px2.|*|.px2.| = 0; then
sqrt(|.px2.|^2) = 1 by SQUARE_1:83; then
A23: |.px2.| = 1 by SQUARE_1:89;
px2 in Ball(0.TOP-REAL n, 1) by A18,Th4; then
consider p2 be Point of TOP-REAL n such that
A24: p2=px2 & |.p2 - 0.TOP-REAL n.| < 1;
thus thesis by A23,A24,RLVECT_1:26;
end;
suppose px2 = 0.TOP-REAL n; hence thesis by A21,EUCLID_2:64; end;
end;
suppose A25: |.px1.| <> 0; then
|.px1.|*|.px1.| < 1*|.px1.| by A16,Th5,XREAL_1:70; then
|.px1.|*|.px1.| < 1 by A16,Th5,XXREAL_0:2; then
-|.px1.|*|.px1.| > -1 by XREAL_1:26; then
A26: -|.px1.|*|.px1.| +1 > -1+1 by XREAL_1:8;
A27: px1 = 1*px1 by EUCLID:33
.= (1-|.px1.|*|.px1.|)/(1-|.px1.|*|.px1.|)*px1 by A26,XCMPLX_1:60
.= (1-|.px1.|*|.px1.|)*((1/(1-|.px1.|*|.px1.|))*px1) by EUCLID:34
.= (1-|.px1.|*|.px1.|)/(1-|.px2.|*|.px2.|)*px2 by A20,EUCLID:34;
A28: px2 <> 0.TOP-REAL n1
proof
assume px2 = 0.TOP-REAL n1; then
px1 = 0.TOP-REAL n1 by A27,EUCLID:32;
hence contradiction by A25,TOPRNS_1:24;
end; then
A29: |.px2.| <> 0 by EUCLID_2:64;
px2 in Ball(0.TOP-REAL n, 1) by A18,Th4; then
consider p2 be Point of TOP-REAL n such that
A30: p2=px2 & |.p2 - 0.TOP-REAL n.| < 1;
A31: |.px2.| < 1 by A30,RLVECT_1:26; then
|.px2.|*|.px2.| < 1*|.px2.| by A29,XREAL_1:70; then
|.px2.|*|.px2.| < 1 by A31,XXREAL_0:2; then
-|.px2.|*|.px2.| > -1 by XREAL_1:26; then
A32: -|.px2.|*|.px2.| +1 > -1+1 by XREAL_1:8;
set l = (1-|.px1.|*|.px1.|)/(1-|.px2.|*|.px2.|);
1/(1-|.px2.|*|.px2.|)*px2
= 1/(1-|.px1.|*|.px1.|)*l*px2 by A27,A20,EUCLID:34; then
1/(1-|.px2.|*|.px2.|)*px2 -1/(1-|.px1.|*|.px1.|)*l*px2
= 0.TOP-REAL n by EUCLID:40; then
1/(1-|.px2.|*|.px2.|)*px2 + (-1/(1-|.px1.|*|.px1.|)*l)*px2
= 0.TOP-REAL n by EUCLID:44; then
A33: (1/(1-|.px2.|*|.px2.|)+ (-1/(1-|.px1.|*|.px1.|)*l))*px2
= 0.TOP-REAL n by EUCLID:37;
A34: l*l = abs(l)*abs(l)
proof
per cases by ABSVALUE:1;
suppose abs l = l; hence thesis; end;
suppose abs l = -l; hence thesis; end;
end;
1/(1-|.px2.|*|.px2.|)+ -1/(1-|.px1.|*|.px1.|)*l = 0
by A28,A33,EUCLID:35; then
1/(1-|.px2.|*|.px2.|) = 1*l/(1-|.px1.|*|.px1.|)
.= 1/((1-|.px1.|*|.px1.|)/l) by XCMPLX_1:78; then
1-|.px2.|*|.px2.| = (1-|.px1.|*|.px1.|)/l by XCMPLX_1:59; then
l*(1-|.px2.|*|.px2.|)
= (1-|.px1.|*|.px1.|)/(l/l) by XCMPLX_1:82
.= (1-|.px1.|*|.px1.|)/1 by A26,A32,XCMPLX_1:60
.= 1-(abs(l)*|.px2.|)*|.l*px2.| by A27,TOPRNS_1:8
.= 1-(abs(l)*|.px2.|)*(abs(l)*|.px2.|) by TOPRNS_1:8
.= 1-abs(l)*abs(l)*|.px2.|*|.px2.|
.= 1-l*l*|.px2.|*|.px2.| by A34; then
(1+l*|.px2.|*|.px2.|)*(1-l) = 0; then
1-l = 0 by A26,A32;
hence x1 = x2 by A27,EUCLID:33;
end;
end; then
A35: f is one-to-one by FUNCT_1:def 8;
consider f0 be 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:30;
consider f1 be 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:92;
consider f2 be Function of TOP-REAL n,R^1 such that
A38: (for p being Point of TOP-REAL n, r1 being real number
st f1.p=r1 holds f2.p=r1*r1) & f2 is continuous by A37,JGRAPH_2:32;
consider f3 be Function of TOP-REAL n,R^1 such that
A39: (for p being Point of TOP-REAL n,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:31;
reconsider 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;
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;
end;
set f4 = f3|Tunit_ball n;
for p being Point of Tunit_ball n holds f4.p <> 0
proof
let p be Point of Tunit_ball n;
assume f4.p = 0; then
A41: f3.p = 0 by FUNCT_1:72;
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;
per cases;
suppose |.p1.| = 0; hence contradiction by A42; end;
suppose |.p1.| <> 0; then
|.p1.|*|.p1.| < 1*|.p1.| by Th5,XREAL_1:70;
hence contradiction by A42,Th5;
end;
end; then
consider f5 be Function of Tunit_ball n,R^1 such that
A43: (for p being Point of Tunit_ball n,r1 being real number st f4.p=r1
holds f5.p=1/r1) & f5 is continuous by JGRAPH_2:36;
consider f6 be Function of Tunit_ball n,TOP-REAL n such that
A44: (for a being Point of Tunit_ball n, b being Point of TOP-REAL n,
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;
assume A46: x in dom f; 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;
f4.p = f3.p by A46,FUNCT_1:72
.= 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;
end; then
A48: f = f6 by A45,FUNCT_1:9;
consider f8 be Function of TOP-REAL n,R^1 such that
A49: (for p being Point of TOP-REAL n,r1 being real number
st f2.p=r1 holds f8.p=4*r1) & f8 is continuous
by A38,JGRAPH_2:33;
consider f9 be Function of TOP-REAL n,R^1 such that
A50: (for p being Point of TOP-REAL n,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:29;
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;
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.|;
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;
set r = 1 + 4*|.p.|*|.p.|;
take r;
thus thesis by A51;
end;
consider f10 be Function of TOP-REAL n,R^1 such that
A53: (for p being Point of TOP-REAL n,r1 being real number
st f9.p=r1 holds f10.p=sqrt(r1)) & f10 is continuous
by A52,A50,JGRAPH_3:15;
consider f11 be Function of TOP-REAL n,R^1 such that
A54: (for p being Point of TOP-REAL n,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:29;
for p being Point of TOP-REAL n holds f11.p <> 0
proof
let p be Point of TOP-REAL n;
A55: f11.p = f0.p + f10.p by A54 .= 1 + f10.p by A36
.= 1 + sqrt(f9.p) by A53;
consider r be real number such that
A56: r = f9.p & r >= 0 by A52;
sqrt(f9.p) >= 0 by A56,SQUARE_1:def 4;
hence thesis by A55;
end; then
consider f12 be Function of TOP-REAL n,R^1 such that
A57: (for p being Point of TOP-REAL n,r1 being real number st f11.p=r1
holds f12.p=1/r1) & f12 is continuous by A54,JGRAPH_2:36;
consider f13 be Function of TOP-REAL n,R^1 such that
A58: (for p being Point of TOP-REAL n,r1 being real number
st f12.p=r1 holds f13.p=2*r1) & f13 is continuous
by A57,JGRAPH_2:33;
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;
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;
end;
reconsider X = TOP-REAL n as non empty SubSpace of TOP-REAL n by TSEP_1:2;
consider f14 be Function of X, TOP-REAL n such that
A60: (for a being Point of X, b being Point of TOP-REAL n,
r being real number st a = b & f13.a = r holds f14.b = r*b) &
f14 is continuous by A58,Th2;
reconsider 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;
per cases by ABSVALUE:1;
suppose abs r = r; hence thesis; end;
suppose abs r = -r; hence thesis; 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;
hereby
assume A63: y in the carrier of Tunit_ball(n);
[#] Tunit_ball(n) c= [#] TOP-REAL n by PRE_TOPC:def 9; 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:66; then
|.q.|*|.q.| < 1 by A63,Th5,XXREAL_0:2; then
A64: 0 < 1 - |.q.|*|.q.| by XREAL_1:52;
set p = 1/(1-|.q.|*|.q.|)*q;
|.p.| = abs(1/(1-|.q.|*|.q.|))*|.q.| by TOPRNS_1:8; then
|.p.|*|.p.| = 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:77
.= |.q.|*|.q.|/((1-|.q.|*|.q.|)*(1-|.q.|*|.q.|)); then
A65: 1 + 4*|.p.|*|.p.|
= ((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:77;
sqrt(1 + 4*|.p.|*|.p.|) = (1+|.q.|*|.q.|)/(1-|.q.|*|.q.|)
by A64,A65,SQUARE_1:89; then
A66: 1+sqrt(1 + 4*|.p.|*|.p.|)
= (1-|.q.|*|.q.|)/(1-|.q.|*|.q.|)+(1+|.q.|*|.q.|)/(1-|.q.|*|.q.|)
by A64,XCMPLX_1:60
.= 2/(1-|.q.|*|.q.|);
reconsider x = p as set;
take x;
thus x in dom f14 by A61;
thus f14.x = f13.p * p by A60
.= 2/(2/(1-|.q.|*|.q.|)) * p by A66,A59
.= (1-|.q.|*|.q.|) * p by XCMPLX_1:52
.= (1-|.q.|*|.q.|)/(1-|.q.|*|.q.|) * q by EUCLID:34
.= 1 * q by A64,XCMPLX_1:60
.= y by EUCLID:33;
end;
given x be set such that
A67: x in dom f14 & y = f14.x;
reconsider p = x as Point of TOP-REAL n1 by A67;
y in rng f14 by A67,FUNCT_1:12; 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:8; 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; then
A69: ((2*2)/((1+sqrt(1 + 4*|.p.|*|.p.|))*(1+sqrt(1 + 4*|.p.|*|.p.|))))*
|.p.|*|.p.| >= 1 by A68,XCMPLX_1:77;
0 <= sqrt(1 + 4*|.p.|*|.p.|) by SQUARE_1:def 4; 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:66; 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 4; then
4*|.p.|*|.p.|-4*|.p.|*|.p.| >= 2+2*sqrt(1 + 4*|.p.|*|.p.|)+4*|.p.|*|.p.|
-4*|.p.|*|.p.| by XREAL_1:11; then
0/2 > 2*sqrt(1 + 4*|.p.|*|.p.|)/2;
hence contradiction by SQUARE_1:def 4;
end; then
|.q.|^2 < 1; then
A70: |.q.| < 1 by SQUARE_1:122;
|. q + -0.TOP-REAL n1 .|<=|.q.| + |. -0.TOP-REAL n1 .| by EUCLID_2:74; then
|. q + -0.TOP-REAL n1 .|<=|.q.| + |. 0.TOP-REAL n1 .| by JGRAPH_5:13; then
|. q + -0.TOP-REAL n1 .|<=|.q.| + 0 by EUCLID_2:61; 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 10;
hence y in the carrier of Tunit_ball(n);
end; then
A71: rng f14 = the carrier of Tunit_ball n by FUNCT_1:def 5; then
reconsider f14 as Function of TOP-REAL n, Tunit_ball n by A61,FUNCT_2:3;
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;
assume A73: x in dom f14;
reconsider g = f as Function;
A74: f" = g" by A14,A35,TOPS_2:def 4;
A75: f14.x in rng f14 by A73,FUNCT_1:12; 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 4;
|.q.| = abs(2/(1+sqrt(1 + 4*|.p.|*|.p.|)))*|.p.| by A77,TOPRNS_1:8; 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:77
.= 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 4
.= 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:92;
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:34
.= (2*(1+sqrt(1 + 4*|.p.|*|.p.|)))/(2*(1+sqrt(1 + 4*|.p.|*|.p.|)))*p
by XCMPLX_1:77
.= 1*p by A78,XCMPLX_1:60 .= p by EUCLID:33; then
[f14.x,x] in f by A76,FUNCT_1:def 4; then
[x,f14.x] in g~ by RELAT_1:def 7; then
[x,f14.x] in g" by A35,FUNCT_1:def 9;
hence f14.x = f".x by A74,FUNCT_1:8;
end; then
f" is continuous by PRE_TOPC:57,A72,FUNCT_1:9;
hence thesis by A3,A14,A35,A44,A48,TOPS_2:def 5;
end;
:: like TOPREALB:19
theorem Th7:
for r being positive (real number),
f being Function of Tunit_ball(n), Tball(p,r) st n <> 0
& for a being Point of Tunit_ball(n), b being Point of TOP-REAL n
st a = b holds f.a = r*b+p
holds f is being_homeomorphism
proof
let r be positive (real number),
f being Function of Tunit_ball(n), Tball(p,r) such that
A1: n <> 0 and
A2: for a being Point of Tunit_ball(n), b being Point of TOP-REAL n st
a = b holds f.a = r*b+p;
reconsider n1 = n as non empty Element of NAT by A1,ORDINAL1:def 13;
reconsider x = p as Point of TOP-REAL n1;
defpred P[Point of TOP-REAL n1,set] means $2 = r*$1+x;
set U = Tunit_ball(n), B = Tball(x,r);
A3: for u being Point of TOP-REAL n1
ex y being Point of TOP-REAL n1 st P[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 P[x,F.x] from FUNCT_2:sch 3(A3);
defpred R[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 R[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 R[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:91;
for p being Point of TOP-REAL n1 holds G.p = 1/r * f1.p + (-1/r) * f2.p
proof
let p be Point of TOP-REAL n1;
thus 1/r * f1.p + (-1/r) * f2.p = 1/r*p + (-1/r)*f2.p by FUNCT_1:35
.= 1/r*p + (-1/r)*x by FUNCOP_1:13 .= 1/r*p - 1/r*x by EUCLID:44
.= 1/r*(p-x) by EUCLID:53 .= G.p by A6;
end; then
A8: G is continuous by TOPALG_1:17;
A9: dom f = [#]U by FUNCT_2:def 1;
A10: dom f = the carrier of U by FUNCT_2:def 1;
for p being Point of TOP-REAL n1 holds F.p = r * f1.p + 1 * f2.p
proof
let p be Point of TOP-REAL n1;
thus r * f1.p + 1 * f2.p = r*f1.p + f2.p by EUCLID:33
.= r*p + f2.p by FUNCT_1:35 .= r*p + x by FUNCOP_1:13 .= F.p by A4;
end;
then
A11: F is continuous by TOPALG_1:17;
A12: the carrier of B = Ball(x,r) by Th4;
A13: the carrier of U = 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 such that
A15: a in dom f;
reconsider y = a as Point of TOP-REAL n1 by A15,PRE_TOPC:55;
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:72;
end;
A16: 1/r*r = 1 by XCMPLX_1:88;
A17: rng f = [#]B
proof
now
let b be set;
assume A18: b in [#]B;
then reconsider c = b as Point of TOP-REAL n1 by PRE_TOPC:55;
reconsider r1=1/r as Real;
set a = r1 * (c - x);
A19: |.a-0.TOP-REAL n1.| = |.a.| by RLVECT_1:26
.= abs(r1)*|. c-x .| by TOPRNS_1:8
.= 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:70; then
A20: a in Ball(0.TOP-REAL n, 1) by A16,A19;
then f.a = r*a+x by A2,A13 .= r*(1/r)*(c-x)+x by EUCLID:34
.= c-x+x by A16,EUCLID:33 .= b by EUCLID:52;
hence b in rng f by A13,A10,A20,FUNCT_1:def 5;
end; then
[#]B c= rng f by TARSKI:def 3;
hence thesis by XBOOLE_0:def 10;
end;
now
let a, b be set such that
A21: a in dom f and
A22: b in dom f and
A23: f.a = f.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:52;
hence a=b by EUCLID:38,52;
end; then
A25: f is one-to-one by FUNCT_1:def 8;
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 such that
A27: a in dom (f");
reconsider y = a as Point of TOP-REAL n1 by A27,PRE_TOPC:55;
reconsider r1=1/r as Real;
set e = 1/r * (y - x);
A28: |.e-0.TOP-REAL n1.| = |.e.| by RLVECT_1:26
.= abs(r1)*|. y-x .| by TOPRNS_1:8 .= 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:70; then
A29: 1/r * (y - x) in Ball(0.TOP-REAL n,1) by A16,A28;
then f.e = r*e+x by A2,A13 .= r*(1/r)*(y-x)+x by EUCLID:34
.= y-x+x by A16,EUCLID:33 .= y by EUCLID:52;
then ff".a = 1/r * (y - x) by A13,A10,A25,A29,FUNCT_1:54;
hence f".a = 1/r*(y-x) by A17,A25,TOPS_2:def 4
.= G.y by A6 .= (G|Ball(x,r)).a by A12,A27,FUNCT_1:72;
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:91; then
A30: f is continuous by A13,A10,A11,A14,BORSUK_4:69,FUNCT_1:9;
A31: dom (f") = the carrier of B by FUNCT_2:def 1;
f" is continuous by A31,A12,A7,A8,A26,BORSUK_4:69,FUNCT_1:9;
hence thesis by A9,A17,A25,A30,TOPS_2:def 5;
end;
theorem Th8:
Tunit_ball n, TOP-REAL n are_homeomorphic
proof
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
set U = Tunit_ball(n), C = TOP-REAL n;
per cases;
suppose A1: n is non empty;
defpred P[Point of U,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 U ex y being Point of C st P[u,y]
proof
let u be Point of U;
reconsider v = u as Point of TOP-REAL n1 by PRE_TOPC:55;
set y = 1/(1-|.v.|*|.v.|)*v;
reconsider y as Point of C;
take y;
thus thesis;
end;
consider f being Function of U,C such that
A3: for x being Point of U holds P[x,f.x] from FUNCT_2:sch 3(A2);
for a being Point of U, b being Point of TOP-REAL n1 st a = b
holds f.a = 1/(1-|.b.|*|.b.|)*b
proof
let a be Point of U, b be Point of TOP-REAL n1;
P[a,f.a] by A3;
hence thesis;
end; then
ex f being Function of U,C st f is being_homeomorphism by A1,Th6;
hence thesis by T_0TOPSP:def 1;
end;
suppose A4: n is empty;
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;
thus x in Ball(0.TOP-REAL 0,1) implies x = 0.TOP-REAL 0;
assume x = 0.TOP-REAL 0; then
reconsider p = x as Point of TOP-REAL 0;
|.p - 0.(TOP-REAL 0).| < 1 by EUCLID_2:61;
hence x in Ball(0.TOP-REAL 0,1);
end;
[#]TOP-REAL 0 = {0.TOP-REAL 0} by JORDAN2C:113,EUCLID:25
.= Ball(0.TOP-REAL 0,1) by A5,TARSKI:def 1;
hence thesis by A4,Th1;
end;
end;
reserve q for Point of TOP-REAL n;
theorem Th9:
for r,s being positive (real number) holds
Tball(p,r), Tball(q,s) are_homeomorphic
proof
let r,s be positive (real number);
per cases;
suppose A1: n is empty;
reconsider n1=n as Element of NAT by ORDINAL1:def 13;
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 iff x in Y
proof
let x be set;
hereby
assume x in X; then
consider x1 be Point of TOP-REAL n such that
A4: x=x1 & |. x1 - p .| < r;
reconsider x1 as Point of TOP-REAL n1;
x1 = 0.TOP-REAL 0 by A1; then
|. x1 - p1 .| = 0 by A2,TOPRNS_1:29;
hence x in Y by A2,A3,A4;
end;
assume x in Y; then
consider x1 be Point of TOP-REAL n such that
A5: x=x1 & |. x1 - q .| < s;
reconsider x1 as Point of TOP-REAL n1;
x1 = 0.TOP-REAL 0 by A1; then
|. x1 - q1 .| = 0 by A3,TOPRNS_1:29;
hence x in X by A2,A3,A5;
end;
hence thesis by TARSKI:2;
end;
suppose n is non empty; then
reconsider n1=n as non empty Element of NAT by ORDINAL1:def 13;
A6: for r being positive (real number), x being Point of TOP-REAL n1
holds Tunit_ball(n1), Tball(x,r) are_homeomorphic
proof
let r be positive (real number), x be Point of TOP-REAL n1;
set U = Tunit_ball(n), C = Tball(x,r);
defpred P[Point of U,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 C = Ball(x,r) by Th4;
A9: for u being Point of U ex y being Point of C st P[u,y]
proof
let u be Point of U;
reconsider v = u as Point of TOP-REAL n1 by PRE_TOPC:55;
set y = r*v+x;
A10: |. y-x .| = |. r*v .| by EUCLID:52
.= abs(r)*|. v .| by A7,TOPRNS_1:8 .= r*|. v .| by ABSVALUE:def 1;
r*|. v .| < r*1 by Th5,XREAL_1:70; then
reconsider y as Point of C by A10,A8,TOPREAL9:7;
take y;
thus thesis;
end;
consider f being Function of U,C such that
A11: for x being Point of U holds P[x,f.x] from FUNCT_2:sch 3(A9);
for a being Point of U, b being Point of TOP-REAL n1 st a = b
holds f.a = r*b+x
proof
let a be Point of U, b be Point of TOP-REAL n1;
P[a,f.a] by A11;
hence thesis;
end; then
ex f being Function of U,C st f is being_homeomorphism by Th7;
hence thesis by T_0TOPSP:def 1;
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;
A12: Tunit_ball(n), Tball(y,s) are_homeomorphic by A6;
Tball(x,r), Tunit_ball(n) are_homeomorphic by A6;
hence thesis by A12,BORSUK_3:3;
end;
hence thesis;
end;
end;
theorem Th10:
for B being non empty ball Subset of TOP-REAL n
holds B, [#]TOP-REAL n are_homeomorphic
proof
let B be non empty ball Subset of TOP-REAL n;
consider p be Point of TOP-REAL n, r be 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;
end;
theorem Th11:
for M, N being non empty TopSpace
for p being Point of M, U being a_neighborhood of p, B being open Subset of N
st U,B are_homeomorphic
ex V being open Subset of M, 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;
let p be Point of M;
let U be a_neighborhood of p;
let B be open Subset of N;
assume U,B are_homeomorphic; then
A1: M|U, N|B are_homeomorphic by METRIZTS:def 1; then
consider f be Function of M|U, N|B such that
A2: f is being_homeomorphism by T_0TOPSP:def 1;
consider V be Subset of M such that
A3: V is open & V c= U & p in V by CONNSP_2:8;
V c= [#](M|U) by A3,PRE_TOPC:def 10; 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:19;
reconsider f1=f as Function of M1, N1;
rng f c= [#](N|B); then
A4: rng f c= B by PRE_TOPC:def 10;
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 as open Subset of M by A3;
B = the carrier of N|B by PRE_TOPC:29; 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 10; 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 5;
V1 = V /\ [#]M1 by XBOOLE_1:28; then
V1 in the topology of M1 by A7,PRE_TOPC:def 9; then
V1 is open by PRE_TOPC:def 5; then
S1 is open by A6; then
reconsider S as open Subset of N by TSEP_1:17;
take V, S;
thus V c= U & p in V by A3;
A8: (M | U) | V1 = M | V by A3,PRE_TOPC:28;
f .: U c= rng f by RELAT_1:144; then
A9: f .: U c= B by A4,XBOOLE_1:1;
f .: V c= f .: U by A3,RELAT_1:156; then
(N | B) | (f .: V1) = N | S by A9,XBOOLE_1:1,PRE_TOPC:28;
hence V,S are_homeomorphic by A5,A8,METRIZTS:def 1;
end;
begin :: Manifold
reserve M for non empty TopSpace;
definition
let n, M;
attr M is n-locally_euclidean means :Def4:
for p being Point of M holds
ex U being a_neighborhood of p, S being open Subset of TOP-REAL n
st U,S are_homeomorphic;
end;
registration
let n;
cluster TOP-REAL n -> n-locally_euclidean;
coherence
proof
let p be Point of TOP-REAL n;
p in [#]TOP-REAL n; then
p in Int [#]TOP-REAL n by TOPS_1:43; 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,S;
thus U,S are_homeomorphic by METRIZTS:1;
end;
end;
registration
let n;
cluster n-locally_euclidean (non empty TopSpace);
correctness
proof take TOP-REAL n; thus thesis; end;
end;
Lm1: M is n-locally_euclidean implies
for p being Point of M holds
ex U being a_neighborhood of p, B being non empty ball Subset of TOP-REAL n
st U,B are_homeomorphic
proof
assume A1: M is n-locally_euclidean;
let p be Point of M;
consider U be a_neighborhood of p, S be open Subset of TOP-REAL n
such that A2: U,S are_homeomorphic by A1,Def4;
consider U1 be open Subset of M, S be open Subset of TOP-REAL n
such that
A3: U1 c= U & p in U1 & U1,S are_homeomorphic by A2,Th11;
reconsider 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 be 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 10;
reconsider S1 = (TOP-REAL n) | S as non empty TopSpace by A4,YELLOW14:19;
reconsider M1 = M|U1 as non empty SubSpace of M;
reconsider f as Function of M1, S1;
A7: [#] ((TOP-REAL n) | S) = S by PRE_TOPC:def 10;
A8: [#] ((TOP-REAL n) | S) c= [#] (TOP-REAL n) by PRE_TOPC:def 9;
f.p in the carrier of (TOP-REAL n) | S by A6,FUNCT_2:7; then
reconsider q = f.p as Point of TOP-REAL n by A8;
consider B be ball Subset of TOP-REAL n such that
A9: B c= S & q in B by A6,FUNCT_2:7,A7,Th3;
reconsider B as non empty ball Subset of TOP-REAL n by A9;
A10: f" is being_homeomorphism by A5,TOPS_2:70;
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:62; then
A14: (f").q in f" .: B1 by A9,FUNCT_1:def 12; then
reconsider U2 = f" .: B1 as non empty Subset of M1;
A15: dom(f"|B1) = B1 by A13,RELAT_1:91;
A16: dom(f"|B1) = [#](S1|B1) by A15,PRE_TOPC:def 10
.= the carrier of S1|B1;
rng(f"|B1) = f" .: B1 by RELAT_1:148
.= [#](M1|U2) by PRE_TOPC:def 10
.= the carrier of M1|U2; then
reconsider g = f"|B1 as Function of S1|B1, M1|U2 by A16,FUNCT_2:3;
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,TOPS_2:def 5,A6;
f1"=f" by A12,TOPS_2:def 4,A11; then
A19: p1 in U2 by A14,A18,FUNCT_1:56;
A20: [#]M1 c= [#]M by PRE_TOPC:def 9;
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 5;
B1 = B /\ [#]S1 by XBOOLE_1:28; then
B1 in the topology of S1 by A21,PRE_TOPC:def 9; then
B1 is open by PRE_TOPC:def 5; then
f" .: B1 is open by A10,TOPGRP_1:25; then
reconsider V as a_neighborhood of p by A19,CONNSP_2:5,CONNSP_2:11;
take V, B;
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 10;
f" .: B1 c= rng(f") by RELAT_1:144; then
A24: M|V = M1|U2 by A23,XBOOLE_1:1,PRE_TOPC:28;
S1|B1 = (TOP-REAL n) | B by A9,PRE_TOPC:28;
hence V,B are_homeomorphic by A24,A22,METRIZTS:def 1;
end;
:: Lemma 2.13a
theorem
M is n-locally_euclidean iff
for p being Point of M holds
ex U being a_neighborhood of p, B being ball Subset of TOP-REAL n
st U,B are_homeomorphic
proof
hereby
assume A1: M is n-locally_euclidean;
let p be Point of M;
consider U be a_neighborhood of p, B be non empty ball Subset of TOP-REAL n
such that A2: U,B are_homeomorphic by A1,Lm1;
reconsider B as ball Subset of TOP-REAL n;
take U, B;
thus U, B are_homeomorphic by A2;
end;
assume A3: for p being Point of M holds
ex U being a_neighborhood of p, B being ball Subset of TOP-REAL n
st U,B are_homeomorphic;
now
let p be Point of M;
consider U be a_neighborhood of p, B be 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, S;
thus U,S are_homeomorphic by A4;
end;
hence M is n-locally_euclidean by Def4;
end;
:: Lemma 2.13b
theorem Th13:
M is n-locally_euclidean iff
for p being Point of M holds
ex U being a_neighborhood of p st U,[#]TOP-REAL n are_homeomorphic
proof
hereby
assume A1: M is n-locally_euclidean;
let p be Point of M;
consider U be a_neighborhood of p, B be non empty ball Subset of TOP-REAL n
such that A2: U,B are_homeomorphic by A1,Lm1;
take U;
A3: (TOP-REAL n) | ([#]TOP-REAL n) = the TopStruct of TOP-REAL n
by TSEP_1:100;
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:19;
A4: U1,B1 are_homeomorphic by A2,METRIZTS:def 1;
B, [#]TOP-REAL n are_homeomorphic by Th10; then
A5: B1, the TopStruct of TOP-REAL n are_homeomorphic by A3,METRIZTS:def 1;
U1, the TopStruct of TOP-REAL n are_homeomorphic by A4,A5,BORSUK_3:3;
hence U,[#]TOP-REAL n are_homeomorphic by A3,METRIZTS:def 1;
end;
assume A6: for p being Point of M holds
ex U being a_neighborhood of p st U,[#]TOP-REAL n are_homeomorphic;
now
let p be Point of M;
consider U be 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: S,[#]TOP-REAL n are_homeomorphic by Th10;
reconsider S as open Subset of TOP-REAL n;
take U, S;
A9: (TOP-REAL n) | ([#]TOP-REAL n) = the TopStruct of TOP-REAL n
by TSEP_1:100;
A10: M|U,the TopStruct of TOP-REAL n are_homeomorphic
by A7,A9,METRIZTS:def 1; then
reconsider U1 = M|U as non empty TopSpace by YELLOW14:19;
reconsider S1 = (TOP-REAL n) | S as non empty TopSpace;
A11: the TopStruct 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;
end;
hence M is n-locally_euclidean by Def4;
end;
registration
let n;
cluster n-locally_euclidean -> first-countable (non empty TopSpace);
correctness
proof
let M be non empty TopSpace;
assume A1: M is n-locally_euclidean;
for p being Point of M ex B being Basis of p st B is countable
proof
let p be Point of M;
consider U be 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, the TopStruct of TOP-REAL n are_homeomorphic by TSEP_1:100; then
consider f be Function of M|U, the TopStruct of TOP-REAL n such that
A3: f is being_homeomorphism by T_0TOPSP:def 1;
A4: dom f = [#](M|U) & rng f = [#](the TopStruct 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 10;
A6: Int U c= U by TOPS_1:44;
A7: p in Int U by CONNSP_2:def 1;
A8: p in dom f by A7,A6,A5;
f.p in rng f by A7,A6,A5,FUNCT_1:12; then
reconsider q=f.p as Point of TOP-REAL n;
reconsider n1=n as Element of NAT by ORDINAL1:def 13;
TOP-REAL n1 is first-countable; then
consider B1 be Basis of q such that
A9: B1 is countable by FRECHET:def 2;
reconsider A = bool the carrier of TOP-REAL n as non empty set;
deffunc F(set) = f" .: $1 /\ Int U;
set B = {F(X) where X is Element of A: X in B1};
A10: card B1 c= omega by A9,CARD_3:def 15;
card B c= card B1 from TREES_2:sch 2; then
A11: card B c= omega by A10,XBOOLE_1:1;
for x being set st x in B holds x in bool the carrier of M
proof
let x be set;
assume x in B; then
consider X1 be Element of A such that
A12: x = F(X1) & X1 in B1;
thus x in bool the carrier of M by A12;
end; then
reconsider B as Subset-Family of M by TARSKI:def 3;
A13: for P being Subset of M st P in B holds P is open
proof
let P be Subset of M;
assume P in B; then
consider X1 be Element of A such that
A14: P = F(X1) & X1 in B1;
reconsider X1 as Subset of the TopStruct of TOP-REAL n;
reconsider X2 = X1 as Subset of TOP-REAL n;
X2 is open by A14,YELLOW_8:21; then
X2 in the topology of TOP-REAL n by PRE_TOPC:def 5; then
A15: X1 is open by PRE_TOPC:def 5;
reconsider U1 = M|U as non empty TopStruct by A7,A6;
reconsider g = f" as Function of the TopStruct of TOP-REAL n, U1;
A16: g is being_homeomorphism by A3,TOPS_2:70;
A17: g .: X1 is open by A15,A16,TOPGRP_1:25;
g .: X1 in the topology of M|U by A17,PRE_TOPC:def 5; then
consider Q be Subset of M such that
A18: Q in the topology of M &
g .: X1 = Q /\ [#](M|U) by PRE_TOPC:def 9;
[#](M|U) = U by PRE_TOPC:def 10; then
A19: P = Q /\ (U /\ Int U) by A18,A14,XBOOLE_1:16
.= Q /\ Int U by TOPS_1:44,XBOOLE_1:28;
Q is open by A18,PRE_TOPC:def 5;
hence P is open by A19;
end;
for Y being set st Y in B holds p in Y
proof
let Y be set;
assume Y in B; then
consider X1 be Element of A such that
A20: Y = F(X1) & X1 in B1;
reconsider g = f as Function;
[p,g.p] in g by A7,A6,A5,FUNCT_1:def 4; then
[q,p] in g~ by RELAT_1:def 7; then
[q,p] in g" by A4,FUNCT_1:def 9; then
A21: [q,p] in f" by A4,TOPS_2:def 4;
q in X1 by A20,YELLOW_8:21; then
p in f" .: X1 by A21,RELAT_1:def 13;
hence p in Y by A20,A7,XBOOLE_0:def 4;
end; then
A22: p in Intersect B by SETFAM_1:58;
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;
assume A23: S is open & p in S;
set S1 = S /\ [#](M|U);
S in the topology of M by A23,PRE_TOPC:def 5; then
A24: S1 in the topology of M|U by PRE_TOPC:def 9;
reconsider U1 = M|U as non empty TopStruct by A7,A6;
reconsider S1 as Subset of U1;
S1 is open by A24,PRE_TOPC:def 5; then
A25: 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 the TopStruct of TOP-REAL n
by A25,PRE_TOPC:def 5; then
A26: S2 is open by PRE_TOPC:def 5;
reconsider g1 = f as Function;
A27: [p,q] in f by A7,A6,A5,FUNCT_1:def 4;
p in S1 by A8,A23,XBOOLE_0:def 4; then
A28: q in S2 by A27,RELAT_1:def 13;
consider W be Subset of TOP-REAL n such that
A29: W in B1 & W c= S2 by A28,A26,YELLOW_8:22;
reconsider W as Element of A;
set V = f" .: W /\ Int U;
reconsider V as Subset of M;
take V;
thus V in B by A29;
A30: g1" = f" by A4,TOPS_2:def 4;
A31: f" .: (f .: S1) = S1 by A30,A4,FUNCT_1:177;
A32: f" .: W /\ Int U c= f" .: W by XBOOLE_1:17;
A33: S1 c= S by XBOOLE_1:17;
f" .: W c= f" .: (f .: S1) by A29,RELAT_1:156; then
f" .: W c= S by A31,A33,XBOOLE_1:1;
hence V c= S by A32,XBOOLE_1:1;
end; then
reconsider B as Basis of p by A13,A22,YELLOW_8:def 2,TOPS_2:def 1;
take B;
thus B is countable by A11,CARD_3:def 15;
end;
hence M is first-countable by FRECHET:def 2;
end;
end;
set T = (TOP-REAL 0) | [#]TOP-REAL 0;
Lm2: T = the TopStruct of TOP-REAL 0 by TSEP_1:100;
registration
cluster 0-locally_euclidean -> discrete (non empty TopSpace);
coherence
proof
let M be non empty TopSpace;
assume A1: M is 0-locally_euclidean;
for X being Subset of M, p being Point of M st X = {p} holds X is open
proof
let X be Subset of M;
let p be Point of M;
assume A2: X = {p};
consider U be a_neighborhood of p such that
A3: U,[#]TOP-REAL 0 are_homeomorphic by A1,Th13;
A4: Int U c= U by TOPS_1:44;
p in Int U by CONNSP_2:def 1; then
A5: p in U by A4;
M|U, T are_homeomorphic by A3,METRIZTS:def 1; then
consider f be Function of M|U, T such that
A6: f is being_homeomorphism by T_0TOPSP:def 1;
consider V be Subset of M such that
A7: V is open & V c= U & p in V by CONNSP_2:8;
for x being set holds x in V iff x = p
proof
let x be set;
hereby
assume x in V; 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 10; then
A10: x in dom f by A6,TOPS_2:def 5; then
A11: f.x in rng f by FUNCT_1:12;
p in [#](M|U) by A5,PRE_TOPC:def 10; then
A12: p in dom f by A6,TOPS_2:def 5; then
A13: f.p in rng f by FUNCT_1:12;
f.x = 0.TOP-REAL 0 by Lm2,A11 .= f.p by Lm2,A13;
hence x = p by A9,A10,A12,FUNCT_1:def 8;
end;
assume x = p;hence x in V by A7;
end;
hence X is open by A2,A7,TARSKI:def 1;
end;
hence M is discrete by TDLAT_3:19;
end;
cluster discrete -> 0-locally_euclidean (non empty TopSpace);
coherence
proof
A14: [#]T = {0.TOP-REAL 0} by EUCLID:25,JORDAN2C:113,Lm2;
let M be non empty TopSpace;
assume A15: M is discrete;
for p being Point of M holds
ex U being a_neighborhood of p st U,[#]TOP-REAL 0 are_homeomorphic
proof
let p be Point of M;
reconsider U = {p} as Subset of M by ZFMISC_1:37;
A16: U is open & p in U by A15,TDLAT_3:17,TARSKI:def 1; then
reconsider U as a_neighborhood of p by CONNSP_2:5;
take U;
set f = {[p, 0.TOP-REAL 0]};
A17: p in [#](M|U) by A16,PRE_TOPC:def 10;
A18: [p, 0.TOP-REAL 0] in [: the carrier of M|U , the carrier of T :]
by A17,ZFMISC_1:106,Lm2;
A19: dom f = U by RELAT_1:23; then
A20: dom f = [#](M|U) by PRE_TOPC:def 10; then
reconsider f as Function of M|U, T by A18,FUNCT_2:def 1,ZFMISC_1:37;
A21: rng f = [#]T by A14,RELAT_1:23;
for P being Subset of M|U holds P is closed iff f .: P is closed
proof
let P be Subset of M|U;
per cases;
suppose A22: P is empty; then f.:P is empty by RELAT_1:149;
hence thesis by A22;
end;
suppose A23: P is non empty; then
P = [#](M|U) by A20,ZFMISC_1:39,A19;
hence P is closed implies f.:P is closed by A21,A20,RELAT_1:146;
thus f.:P is closed implies P is closed by A23,A20,ZFMISC_1:39,A19;
end;
end; then
f is being_homeomorphism by A20,A21,TOPS_2:72; then
M|U, T are_homeomorphic by T_0TOPSP:def 1;
hence U,[#]TOP-REAL 0 are_homeomorphic by METRIZTS:def 1;
end;
hence M is 0-locally_euclidean by Th13;
end;
end;
registration
let n;
cluster TOP-REAL n -> second-countable;
correctness
proof
set T = the TopStruct of TOP-REAL n;
A1: for x being set holds
x in {card B where B is Basis of T : not contradiction} iff
x in {card B where B is Basis of TOP-REAL n : not contradiction}
proof
let x be set;
hereby
assume x in {card B where B is Basis of T : not contradiction}; then
consider B1 be Basis of T 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 : not contradiction};
end;
assume x in {card B where B is Basis of TOP-REAL n : not contradiction};
then consider B1 be Basis of TOP-REAL n such that
A3: x = card B1;
reconsider B2=B1 as Basis of T by YELLOW12:32;
x = card B2 by A3;
hence x in {card B where B is Basis of T : not contradiction};
end;
weight T = weight TOP-REAL n by A1,TARSKI:2; then
weight TOP-REAL n c= omega by WAYBEL23:def 6;
hence thesis by WAYBEL23:def 6;
end;
end;
registration
let n;
cluster second-countable Hausdorff n-locally_euclidean (non empty TopSpace);
existence
proof take TOP-REAL n; thus thesis; end;
end;
definition
let n, M;
attr M is n-manifold means :Def5:
M is second-countable Hausdorff n-locally_euclidean;
end;
definition
let M;
attr M is manifold-like means :Def6:
ex n st M is n-manifold;
end;
registration
let n;
cluster n-manifold (non empty TopSpace);
existence
proof
take TOP-REAL n;
thus thesis by Def5;
end;
end;
registration
let n;
cluster n-manifold ->
second-countable Hausdorff n-locally_euclidean (non empty TopSpace);
correctness by Def5;
cluster second-countable Hausdorff n-locally_euclidean ->
n-manifold (non empty TopSpace);
correctness by Def5;
cluster n-manifold -> manifold-like (non empty TopSpace);
correctness by Def6;
end;
registration
cluster second-countable discrete -> 0-manifold (non empty TopSpace);
coherence;
end;
:: Lemma 2.16
registration
let n;
let M be n-manifold (non empty TopSpace);
cluster open -> n-manifold (non empty SubSpace of M);
correctness
proof
let X be non empty SubSpace of M;
assume A1: X is open;
[#]X c= [#]M by PRE_TOPC:def 9; 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 10
.= the carrier of M|X1; then
A3: the TopStruct of X = the TopStruct of M|X1 by TSEP_1:5;
A4: for x being set holds
x in {card B where B is Basis of X : not contradiction} iff
x in {card B where B is Basis of M|X1 : not contradiction}
proof
let x be set;
hereby
assume x in {card B where B is Basis of X : not contradiction}; then
consider B1 be 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 : not contradiction};
end;
assume x in {card B where B is Basis of M|X1 : not contradiction};
then consider B1 be 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 : not contradiction};
end;
weight X = weight M|X1 by A4,TARSKI:2; 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 holds
ex U being a_neighborhood of p, S being open Subset of TOP-REAL n
st U,S are_homeomorphic
proof
let p be Point of X;
p in the carrier of X; then
reconsider p1 = p as Point of M by A2;
consider U1 be a_neighborhood of p1, S1 be open Subset of TOP-REAL n
such that
A8: U1, S1 are_homeomorphic by Def4;
consider U2 be open Subset of M, S2 be 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 open (non empty 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 be 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 as a_neighborhood of p by A12,CONNSP_2:5;
U c= U2 by XBOOLE_1:17; then
U c= [#](M|U2) by PRE_TOPC:def 10; 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:19;
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 10;
A16: X1 in the topology of M by PRE_TOPC:def 5;
U2 = [#]M2 by PRE_TOPC:def 10; then
U3 in the topology of M2 by A16,PRE_TOPC:def 9; then
U3 is open by PRE_TOPC:def 5; then
reconsider S = f.:U3 as open Subset of T2 by A14;
S in the topology of T2 by PRE_TOPC:def 5; then
consider Q be Subset of TOP-REAL n such that
A17: Q in the topology of TOP-REAL n & S=Q/\([#]T2) by PRE_TOPC:def 9;
A18: [#]T2 = S2 by PRE_TOPC:def 10;
S2 in the topology of TOP-REAL n by PRE_TOPC:def 5; then
S in the topology of TOP-REAL n by A18,A17,PRE_TOPC:def 1; then
reconsider S as open Subset of TOP-REAL n by PRE_TOPC:def 5;
take U, S;
U c= X1; then U c= [#](M|X1) by PRE_TOPC:def 10; then
reconsider U4 = U as Subset of M|X1;
reconsider U5 = U as Subset of M;
A19: M|X1|U4 = M|U5 by GOBOARD9:4;
M|U2|U3 = M|U5 by GOBOARD9:4; then
A20: the TopStruct of X|U = the TopStruct of M|U2|U3
by A19,A3,PRE_TOPC:66;
((TOP-REAL n) | S2) | (f.:U3) = (TOP-REAL n) | S by A15,PRE_TOPC:28;
hence U, S are_homeomorphic by A13,A20,METRIZTS:def 1;
end; then
X is n-locally_euclidean by Def4;
hence X is n-manifold by A7;
end;
end;
registration
cluster manifold-like (non empty TopSpace);
existence
proof
take TOP-REAL 0;
thus thesis;
end;
end;
definition
mode manifold is manifold-like (non empty TopSpace);
end;