:: The Definition of Topological Manifolds
:: by Marco Riccardi
::
:: Received August 17, 2010
:: Copyright (c) 2010-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, 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_0, MFOLD_1, FUNCT_2, NAT_1,
XCMPLX_0, BROUWER;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, FUNCT_1, TOPS_2, RELAT_1,
RELSET_1, FUNCT_2, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0,
COMPLEX1, STRUCT_0, PRE_TOPC, METRIC_1, TOPREAL9, TOPS_1, RLVECT_1,
BORSUK_3, CONNSP_2, TSEP_1, METRIZTS, PCOMPS_1, COMPTS_1, EUCLID,
SQUARE_1, TOPMETR, TMAP_1, XXREAL_1, MEMBERED, XXREAL_2, WAYBEL23,
CANTOR_1, CARD_1, TDLAT_3, ZFMISC_1, CARD_3, YELLOW_8, FRECHET, BROUWER,
MFOLD_0;
constructors TOPREAL9, TOPREALB, SQUARE_1, FUNCSDOM, TOPS_1, BORSUK_3,
METRIZTS, COMPLEX1, BINOP_2, TMAP_1, WAYBEL23, CANTOR_1, TDLAT_3,
YELLOW_8, FRECHET, SEQ_4, NUMBERS, BROUWER, MFOLD_0;
registrations XBOOLE_0, XXREAL_0, XREAL_0, XCMPLX_0, NAT_1, MEMBERED,
STRUCT_0, EUCLID, VALUED_0, FINSEQ_1, FUNCT_1, RELAT_1, PRE_TOPC, TOPS_1,
CARD_1, TSEP_1, TOPREAL9, COMPLEX1, TMAP_1, TOPMETR, XXREAL_2, TOPREAL1,
YELLOW13, KURATO_2, SUBSET_1, RELSET_1, FUNCT_2, SQUARE_1, MFOLD_0;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
definitions TARSKI, FUNCT_1;
equalities XCMPLX_0, ALGSTR_0, STRUCT_0, PCOMPS_1, TOPREAL9, SQUARE_1, TMAP_1,
ORDINAL1, MFOLD_0;
expansions TARSKI, FUNCT_1;
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,
RLVECT_4, BROUWER, BROUWER3, MFOLD_0;
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 object;
assume x1 in dom f & x2 in dom f & f.x1 = f.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;
end;
end;
reserve n for Nat;
::$CT
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
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
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;
[#] X c= [#] TOP-REAL n by PRE_TOPC:def 4; then
reconsider p = x as Point of TOP-REAL n;
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
A3: for x being Element of X holds for b being Point of TOP-REAL n,
r being Real 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;
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
reconsider gp = g.p as Point of Euclid n by TOPREAL3:8;
[#] X c= [#] TOP-REAL n by PRE_TOPC:def 4; then
reconsider pp = p as Point of TOP-REAL n1;
reconsider fp = f.p as Real;
assume g.p in V & V is open; then
g.p in Int V by TOPS_1:23; then
consider r0 be Real such that
A4: r0 > 0 and
A5: Ball(gp,r0) c= V by GOBOARD6:5;
per cases;
suppose A6: 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 2; then
W2 in the topology of X by PRE_TOPC:def 4; then
A7: W2 is open by PRE_TOPC:def 2;
p in Ball(pp, r0/2) by A4,JORDAN:16; then
A8: p in W2 by XBOOLE_0:def 4;
set WW2 = {|.p2.| where p2 is Point of TOP-REAL n: p2 in W2};
A9: |.pp.| in WW2 by A8;
for x being object st x in WW2 holds x is real
proof
let x be object;
assume x in WW2; then
consider p2 be Point of TOP-REAL n1 such that
A10: x = |.p2.| & p2 in W2;
thus x is real by A10;
end; then
reconsider WW2 as non empty real-membered set by A9,MEMBERED:def 3;
for x being ExtReal st x in WW2 holds
x <= |.pp.|+r0/2
proof
let x be ExtReal;
assume x in WW2; then
consider p2 be Point of TOP-REAL n1 such that
A11: x = |.p2.| & p2 in W2;
p2 in Ball(pp, r0/2) by A11,XBOOLE_0:def 4; then
A12: |. 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 A12,XXREAL_0:2; then
|.p2.| - |.pp.| + |.pp.| <= r0/2 + |.pp.| by XREAL_1:6;
hence x <= |.pp.|+r0/2 by A11;
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;
A13: m >= 0
proof
assume A14: m < 0;
A15: m is UpperBound of WW2 by XXREAL_2:def 3;
|.pp.| in WW2 by A8;
hence contradiction by A14,A15,XXREAL_2:def 1;
end;
per cases by A13;
suppose A16: m = 0;
set G1 = REAL;
REAL in the topology of R^1 by PRE_TOPC:def 1,TOPMETR:17; then
reconsider G1 as open Subset of R^1 by PRE_TOPC:def 2;
fp in G1 by XREAL_0:def 1; then
consider W1 be Subset of X such that
A17: p in W1 and
A18: W1 is open and
f.:W1 c= G1 by A1,JGRAPH_2:10;
reconsider W3 = W1 /\ W2 as Subset of X;
take W3;
thus p in W3 by A17,A8,XBOOLE_0:def 4;
thus W3 is open by A18,A7;
g.:W3 c= Ball(gp,r0)
proof
let x be object;
assume x in g.:W3; then
consider q be object such that
A19: q in dom g and
A20: q in W3 and
A21: g.q = x by FUNCT_1:def 6;
reconsider q as Point of X by A19;
[#] X c= [#] TOP-REAL n by PRE_TOPC:def 4; then
reconsider qq = q as Point of TOP-REAL n1;
reconsider fq = f.q as Real;
A22: x = fq * qq by A3,A21; 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 A22;
A23: gpp = fp * pp by A3;
reconsider r2 = fq-fp as Real;
A24: |.fq-fp.|*|.qq.| = |.r2.|*|.qq.| .= |.(fq-fp)*qq.|
by TOPRNS_1:7;
qq in W2 by A20,XBOOLE_0:def 4; then
|.qq.| in WW2; then
A25: |.qq.| <= m by XXREAL_2:4;
A26: gpp = 0.TOP-REAL n1 by A23,A6,RLVECT_1:10;
|. gqq + -gpp .| <= |. gqq .| + |. -gpp .| by EUCLID_2:52; then
|. gqq + -gpp .| <= |. gqq .| + |. 0.TOP-REAL n1 .|
by A26,JGRAPH_5:10; then
|. gqq + -gpp .| <= |. gqq .| + 0 by EUCLID_2:39; then
|. gqq - gpp .| < r0 by A3,A21,A6,A25,A24,A4,A16; then
gqq in Ball(gpp,r0);
hence x in Ball(gp,r0) by TOPREAL9:13;
end;
hence thesis by A5;
end;
suppose A27: m > 0;
set G1 = ]. fp-r0/m, fp+r0/m .[;
reconsider G1 as open Subset of R^1
by JORDAN6:35,TOPMETR:17,XXREAL_1:225;
A28: 0 + fp < r0/m + fp by A27,A4,XREAL_1:6;
-r0/m + fp < 0 + fp by A27,A4,XREAL_1:6; then
consider W1 be Subset of X such that
A29: p in W1 and
A30: W1 is open and
A31: f.:W1 c= G1 by A1,JGRAPH_2:10,A28,XXREAL_1:4;
reconsider W3 = W1 /\ W2 as Subset of X;
take W3;
thus p in W3 by A29,A8,XBOOLE_0:def 4;
thus W3 is open by A30,A7;
g.:W3 c= Ball(gp,r0)
proof
let x be object;
assume x in g.:W3; then
consider q be object such that
A32: q in dom g and
A33: q in W3 and
A34: g.q = x by FUNCT_1:def 6;
reconsider q as Point of X by A32;
A35: 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;
reconsider fq = f.q as Real;
A36: x = fq * qq by A3,A34; 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 A36;
A37: gpp = fp * pp by A3;
reconsider r2 = fq as Real;
A38: |.fq.|*|.qq.| = |.r2.|*|.qq.| .= |.fq*qq.|
by TOPRNS_1:7;
A39: q in dom f by A35,FUNCT_2:def 1;
q in W1 by A33,XBOOLE_0:def 4; then
f.q in f.:W1 by A39,FUNCT_1:def 6; then
|.fq-fp.| < r0/m by A31,RCOMP_1:1; then
|.fq.|*m < r0/m*m by A6,A27,XREAL_1:68; then
|.fq.|*m < r0/(m/m) by XCMPLX_1:82; then
A40: |.fq.|*m < r0/1 by A27,XCMPLX_1:60;
qq in W2 by A33,XBOOLE_0:def 4; then
|.qq.| in WW2; then
|.qq.| <= m by XXREAL_2:4; then
A41: |.qq.|*|.fq.| <= m*|.fq.| by XREAL_1:64;
A42: gpp = 0.TOP-REAL n1 by A37,A6,RLVECT_1:10;
A43: |. gqq .| < r0 by A36,A41,A38,A40,XXREAL_0:2;
|. gqq + -gpp .| <= |. gqq .| + |. -gpp .| by EUCLID_2:52; then
|. gqq + -gpp .| <= |. gqq .| + |. 0.TOP-REAL n1 .|
by A42,JGRAPH_5:10; then
|. gqq + -gpp .| <= |. gqq .| + 0 by EUCLID_2:39; then
|. gqq - gpp .| < r0 by A43,XXREAL_0:2; then
gqq in Ball(gpp,r0);
hence x in Ball(gp,r0) by TOPREAL9:13;
end;
hence thesis by A5;
end;
end;
suppose A44: fp <> 0;
reconsider W2 = Ball(pp, r0/2/|.fp.|) /\ [#]X as Subset of X;
Ball(pp, r0/2/|.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
A45: W2 is open by PRE_TOPC:def 2;
p in Ball(pp, r0/2/|.fp.|) by A44,A4,JORDAN:16; then
A46: p in W2 by XBOOLE_0:def 4;
set WW2 = {|.p2.| where p2 is Point of TOP-REAL n: p2 in W2};
A47: |.pp.| in WW2 by A46;
for x being object st x in WW2 holds x is real
proof
let x be object;
assume x in WW2; then
consider p2 be Point of TOP-REAL n1 such that
A48: x = |.p2.| & p2 in W2;
thus x is real by A48;
end; then
reconsider WW2 as non empty real-membered set by A47,MEMBERED:def 3;
for x being ExtReal st x in WW2 holds
x <= |.pp.|+r0/2/|.fp.|
proof
let x be ExtReal;
assume x in WW2; then
consider p2 be Point of TOP-REAL n1 such that
A49: x = |.p2.| & p2 in W2;
p2 in Ball(pp, r0/2/|.fp.|) by A49,XBOOLE_0:def 4; then
A50: |. p2 - pp .| < r0/2/|.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/|.fp.| by A50,XXREAL_0:2; then
|.p2.| - |.pp.| + |.pp.| <= r0/2/|.fp.| + |.pp.| by XREAL_1:6;
hence x <= |.pp.|+r0/2/|.fp.| by A49;
end; then
|.pp.|+r0/2/|.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;
A51: m >= 0
proof
assume A52: m < 0;
A53: m is UpperBound of WW2 by XXREAL_2:def 3;
|.pp.| in WW2 by A46;
hence contradiction by A52,A53,XXREAL_2:def 1;
end;
per cases by A51;
suppose A54: m = 0;
set G1 = REAL;
REAL in the topology of R^1 by PRE_TOPC:def 1,TOPMETR:17; then
reconsider G1 as open Subset of R^1 by PRE_TOPC:def 2;
fp in G1 by XREAL_0:def 1; then
consider W1 be Subset of X such that
A55: p in W1 and
A56: W1 is open and
f.:W1 c= G1 by A1,JGRAPH_2:10;
reconsider W3 = W1 /\ W2 as Subset of X;
take W3;
thus p in W3 by A55,A46,XBOOLE_0:def 4;
thus W3 is open by A56,A45;
g.:W3 c= Ball(gp,r0)
proof
let x be object;
assume x in g.:W3; then
consider q be object such that
A57: q in dom g and
A58: q in W3 and
A59: g.q = x by FUNCT_1:def 6;
reconsider q as Point of X by A57;
[#] X c= [#] TOP-REAL n by PRE_TOPC:def 4; then
reconsider qq = q as Point of TOP-REAL n1;
reconsider fq = f.q as Real;
A60: x = fq * qq by A3,A59; 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 A60;
A61: gpp = fp * pp by A3;
reconsider r2 = fq-fp as Real;
reconsider r3 = fp as Real;
A62: |.fq-fp.|*|.qq.| = |.r2.|*|.qq.| .= |.(fq-fp)*qq.|
by TOPRNS_1:7;
qq in W2 by A58,XBOOLE_0:def 4; then
|.qq.| in WW2; then
A63: |.qq.| <= m by XXREAL_2:4;
A64: |.fp.|*|.qq-pp.| = |.r3.|*|.qq-pp.| .= |.fp*(qq-pp).|
by TOPRNS_1:7;
qq in W2 by A58,XBOOLE_0:def 4; then
qq in Ball(pp, r0/2/|.fp.|) by XBOOLE_0:def 4; then
|.fp.|*|.qq-pp.| < |.fp.|*(r0/2/|.fp.|)
by A44,XREAL_1:68,TOPREAL9:7; then
|.fp.|*|.qq-pp.| < r0/2/(|.fp.|/|.fp.|) by XCMPLX_1:81; then
A65: |.fp.|*|.qq-pp.| < r0/2/1 by A44,XCMPLX_1:60;
A66: |.(fq-fp)*qq.| + |.fp*(qq-pp).| < r0/2+r0/2
by A63,A65,A64,A62,A54,XREAL_1:8;
|.(fq-fp)*qq + fp*(qq-pp).| <= |.(fq-fp)*qq.| + |.fp*(qq-pp).|
by EUCLID_2:52; then
A67: |.(fq-fp)*qq + fp*(qq-pp).| < r0 by A66,XXREAL_0:2;
(fq-fp)*qq + fp*(qq-pp) = fq*qq -fp*qq + fp*(qq-pp) by RLVECT_1:35
.= fq*qq -fp*qq + (fp*qq -fp*pp) by RLVECT_1:34
.= fq*qq -fp*qq +fp*qq -fp*pp by RLVECT_1:def 3
.= fq*qq - fp*pp by RLVECT_4:1; then
gqq in Ball(gpp,r0) by A60,A67,A61;
hence x in Ball(gp,r0) by TOPREAL9:13;
end;
hence thesis by A5;
end;
suppose A68: m > 0;
set G1 = ]. fp-r0/2/m, fp+r0/2/m .[;
reconsider G1 as open Subset of R^1
by JORDAN6:35,TOPMETR:17,XXREAL_1:225;
A69: 0 + fp < r0/2/m + fp by A68,A4,XREAL_1:6;
-r0/2/m + fp < 0 + fp by A68,A4,XREAL_1:6; then
consider W1 be Subset of X such that
A70: p in W1 and
A71: W1 is open and
A72: f.:W1 c= G1 by A1,JGRAPH_2:10,A69,XXREAL_1:4;
reconsider W3 = W1 /\ W2 as Subset of X;
take W3;
thus p in W3 by A70,A46,XBOOLE_0:def 4;
thus W3 is open by A71,A45;
g.:W3 c= Ball(gp,r0)
proof
let x be object;
assume x in g.:W3; then
consider q be object such that
A73: q in dom g and
A74: q in W3 and
A75: g.q = x by FUNCT_1:def 6;
reconsider q as Point of X by A73;
A76: 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;
reconsider fq = f.q as Real;
A77: x = fq * qq by A3,A75; 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 A77;
A78: gpp = fp * pp by A3;
reconsider r2 = fq-fp as Real;
reconsider r3 = fp as Real;
A79: |.fq-fp.|*|.qq.| = |.r2.|*|.qq.|
.= |.(fq-fp)*qq.| by TOPRNS_1:7;
A80: q in dom f by A76,FUNCT_2:def 1;
q in W1 by A74,XBOOLE_0:def 4; then
f.q in f.:W1 by A80,FUNCT_1:def 6; then
|.fq-fp.|*m < r0/2/m*m by A68,XREAL_1:68,A72,RCOMP_1:1; then
|.fq-fp.|*m < r0/2/(m/m) by XCMPLX_1:82; then
A81: |.fq-fp.|*m < r0/2/1 by A68,XCMPLX_1:60;
qq in W2 by A74,XBOOLE_0:def 4; then
|.qq.| in WW2; then
|.qq.| <= m by XXREAL_2:4; then
|.qq.|*|.fq-fp.| <= m*|.fq-fp.| by XREAL_1:64; then
A82: |.(fq-fp)*qq.| < r0/2 by A79,A81,XXREAL_0:2;
A83: |.fp.|*|.qq-pp.| = |.r3.|*|.qq-pp.| .= |.fp*(qq-pp).|
by TOPRNS_1:7;
qq in W2 by A74,XBOOLE_0:def 4; then
qq in Ball(pp, r0/2/|.fp.|) by XBOOLE_0:def 4; then
|.fp.|*|.qq-pp.| < |.fp.|*(r0/2/|.fp.|)
by A44,XREAL_1:68,TOPREAL9:7; then
|.fp.|*|.qq-pp.| < r0/2/(|.fp.|/|.fp.|) by XCMPLX_1:81; then
A84: |.fp.|*|.qq-pp.| < r0/2/1 by A44,XCMPLX_1:60;
A85: |.(fq-fp)*qq.| + |.fp*(qq-pp).| < r0/2+r0/2
by A82,A84,A83,XREAL_1:8;
|.(fq-fp)*qq + fp*(qq-pp).| <= |.(fq-fp)*qq.| + |.fp*(qq-pp).|
by EUCLID_2:52; then
A86: |.(fq-fp)*qq + fp*(qq-pp).| < r0 by A85,XXREAL_0:2;
(fq-fp)*qq + fp*(qq-pp) = fq*qq -fp*qq + fp*(qq-pp) by RLVECT_1:35
.= fq*qq -fp*qq + (fp*qq -fp*pp) by RLVECT_1:34
.= fq*qq -fp*qq +fp*qq -fp*pp by RLVECT_1:def 3
.= fq*qq - fp*pp by RLVECT_4:1; then
gqq in Ball(gpp,r0) by A77,A78,A86;
hence x in Ball(gp,r0) by TOPREAL9:13;
end;
hence thesis by A5;
end;
end;
end;
hence thesis by A3,JGRAPH_2:10;
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 st S = Ball(p,r);
end;
registration
let n;
cluster ball for Subset of TOP-REAL n;
correctness
proof
take Ball(the Point of TOP-REAL n,the Real);
thus thesis;
end;
cluster ball -> open for Subset of TOP-REAL n;
correctness;
end;
registration
let n;
cluster non empty ball for 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;
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 2;
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 4;
reconsider r as positive Real 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;
reconsider p1=p as Point of TOP-REAL n1;
Ball(x,r) = Ball(p1,r) by TOPREAL9:13;
hence thesis by A4,GOBOARD6:1;
end;
definition
::$CD
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;
end;
::$CT
theorem Th5:
n <> 0 & p is Point of Tunit_ball(n) implies |. p .| < 1
proof
reconsider j = 1 as Real;
assume n <> 0; then
reconsider n1 = n as non zero Element of NAT by ORDINAL1:def 12;
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 MFOLD_0:2;
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 4;
reconsider n1 = n as non zero Element of NAT by A1,ORDINAL1:def 12;
for y being object st y in [#]TOP-REAL n1
ex x being object st [x,y] in f
proof
let y be object;
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:13; then
x in Ball(0.TOP-REAL n, 1); then
A6: x in dom f by A3,MFOLD_0:2;
take x;
f.x = 1/(1-|.x.|*|.x.|)*x by A6,A2
.= py by A5,RLVECT_1:def 8;
hence [x,y] in f by A6,FUNCT_1:def 2;
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 2;
A9: |.x.| = |.r.|*|.py.| by TOPRNS_1:7
.= r*|.py.| by A8,ABSVALUE:def 1;
|.x.| < 1
proof
|.py.|*4 + (1+4*p2) > 0 + (1+4*p2) by A7,XREAL_1:6; then
sqrt((1+2*|.py.|)^2) > sqrt(1+4*p2) by SQUARE_1:27; then
1+2*|.py.| > sqrt(1+4*p2) by SQUARE_1:22; then
1+2*|.py.|-sqrt(1+4*p2) > sqrt(1+4*p2)-sqrt(1+4*p2) by XREAL_1:9; then
1-sqrt(1+4*p2)+2*|.py.|-2*|.py.| > 0 - 2*|.py.| by XREAL_1:9; 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 2; 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:24; then
(2*|.py.|)*((2*|.py.|)/(1+sqrt(1+4*p2)))/(2*|.py.|)
< 2*|.py.|/(2*|.py.|) by A7,XREAL_1:74; 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:77; 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:13; then
x in Ball(0.TOP-REAL n1, 1); then
A10: x in dom f by A3,MFOLD_0:2;
take x;
A11: sqrt(1+4*p2)>=0 by SQUARE_1:def 2;
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 2;
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:76
.= 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 2
.= 4/(2*(1+sqrt(1+4*p2)+2*p2))*p2
.= 4/2/(1+sqrt(1+4*p2)+2*p2)*p2 by XCMPLX_1:78
.= (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:76
.= (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 2
.= (-4*p2)/(1+2*p2-2*p2*sqrt(1+4*p2)-(1+4*p2)) by SQUARE_1:def 2
.= (-4*p2)/((-2*p2)*(1+sqrt(1+4*p2)))
.= 2*(-2*p2)/(-2*p2)/(1+sqrt(1+4*p2)) by XCMPLX_1:78
.= 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,RLVECT_1:def 7
.= 1*py by A8,XCMPLX_1:60
.= py by RLVECT_1:def 8;
hence [x,y] in f by A10,FUNCT_1:def 2;
end;
end; then
A14: rng f = [#]TOP-REAL n1 by RELSET_1:10;
for x1,x2 being object st x1 in dom f & x2 in dom f & f.x1 = f.x2 holds
x1 = x2
proof
let x1,x2 be object;
A15: [#]Tunit_ball n c= [#] TOP-REAL n by PRE_TOPC:def 4;
assume A16: x1 in dom f; 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;
reconsider px2 = x2 as Point of TOP-REAL n1 by A17,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 1/(1-|.px2.|*|.px2.|)*px2 = 0.TOP-REAL n
by A20,RLVECT_1:10,EUCLID_2:42;
then per cases by RLVECT_1:11;
suppose 1/(1-|.px2.|*|.px2.|) = 0; then
1-|.px2.|*|.px2.| = 0; then
sqrt(|.px2.|^2) = 1; then
A22: |.px2.| = 1 by SQUARE_1:22;
px2 in Ball(0.TOP-REAL n, 1) by A18,MFOLD_0:2; then
consider p2 be Point of TOP-REAL n such that
A23: p2=px2 & |.p2 - 0.TOP-REAL n.| < 1;
thus thesis by A22,A23,RLVECT_1:13;
end;
suppose px2 = 0.TOP-REAL n; hence thesis by A21,EUCLID_2:42; end;
end;
suppose A24: |.px1.| <> 0; 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
A25: -|.px1.|*|.px1.| +1 > -1+1 by XREAL_1:6;
A26: px1 = 1*px1 by RLVECT_1:def 8
.= (1-|.px1.|*|.px1.|)/(1-|.px1.|*|.px1.|)*px1 by A25,XCMPLX_1:60
.= (1-|.px1.|*|.px1.|)*((1/(1-|.px1.|*|.px1.|))*px1) by RLVECT_1:def 7
.= (1-|.px1.|*|.px1.|)/(1-|.px2.|*|.px2.|)*px2 by A20,RLVECT_1:def 7;
A27: px2 <> 0.TOP-REAL n1
proof
assume px2 = 0.TOP-REAL n1; then
px1 = 0.TOP-REAL n1 by A26,RLVECT_1:10;
hence contradiction by A24,TOPRNS_1:23;
end; then
A28: |.px2.| <> 0 by EUCLID_2:42;
px2 in Ball(0.TOP-REAL n, 1) by A18,MFOLD_0:2; then
consider p2 be Point of TOP-REAL n such that
A29: p2=px2 & |.p2 - 0.TOP-REAL n.| < 1;
A30: |.px2.| < 1 by A29,RLVECT_1:13; then
|.px2.|*|.px2.| < 1*|.px2.| by A28,XREAL_1:68; then
|.px2.|*|.px2.| < 1 by A30,XXREAL_0:2; then
-|.px2.|*|.px2.| > -1 by XREAL_1:24; then
A31: -|.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.|)*l*px2 by A26,A20,RLVECT_1:def 7; then
1/(1-|.px2.|*|.px2.|)*px2 -1/(1-|.px1.|*|.px1.|)*l*px2
= 0.TOP-REAL n by RLVECT_1:5; then
1/(1-|.px2.|*|.px2.|)*px2 + (-1/(1-|.px1.|*|.px1.|)*l)*px2
= 0.TOP-REAL n by RLVECT_1:79; then
A32: (1/(1-|.px2.|*|.px2.|)+ (-1/(1-|.px1.|*|.px1.|)*l))*px2
= 0.TOP-REAL n by RLVECT_1:def 6;
A33: l*l = |.l.|*|.l.|
proof
per cases by ABSVALUE:1;
suppose |.l.| = l; hence thesis; end;
suppose |.l.| = -l; hence thesis; end;
end;
1/(1-|.px2.|*|.px2.|)+ -1/(1-|.px1.|*|.px1.|)*l = 0
by A27,A32,RLVECT_1:11; then
1/(1-|.px2.|*|.px2.|) = 1*l/(1-|.px1.|*|.px1.|)
.= 1/((1-|.px1.|*|.px1.|)/l) by XCMPLX_1:77; 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:81
.= (1-|.px1.|*|.px1.|)/1 by A25,A31,XCMPLX_1:60
.= 1-(|.l.|*|.px2.|)*|.l*px2.| by A26,TOPRNS_1:7
.= 1-(|.l.|*|.px2.|)*(|.l.|*|.px2.|) by TOPRNS_1:7
.= 1-|.l.|*|.l.|*|.px2.|*|.px2.|
.= 1-l*l*|.px2.|*|.px2.| by A33; then
(1+l*|.px2.|*|.px2.|)*(1-l) = 0; then
1-l = 0 by A25,A31;
hence x1 = x2 by A26,RLVECT_1:def 8;
end;
end; then
A34: f is one-to-one;
consider f0 be Function of TOP-REAL n1, R^1 such that
A35: (for p being Point of TOP-REAL n1 holds f0.p=1) & f0 is continuous
by JGRAPH_2:20;
consider f1 be Function of TOP-REAL n1, R^1 such that
A36: (for p being Point of TOP-REAL n1 holds f1.p = |.p.|)
& f1 is continuous by JORDAN2C:84;
consider f2 be Function of TOP-REAL n,R^1 such that
A37: (for p being Point of TOP-REAL n, r1 being Real
st f1.p=r1 holds f2.p=r1*r1) & f2 is continuous by A36,JGRAPH_2:22;
consider f3 be Function of TOP-REAL n,R^1 such that
A38: (for p being Point of TOP-REAL n,r1,r2 being Real
st f0.p=r1 & f2.p=r2 holds f3.p=r1-r2) & f3 is continuous
by A35,A37,JGRAPH_2:21;
reconsider f3 as continuous Function of TOP-REAL n,R^1 by A38;
A39: 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 A38 .= 1 - f2.p by A35
.= 1 - f1.p*f1.p by A37 .= 1 - |.p.|*f1.p by A36
.= 1 - |.p.|*|.p.| by A36;
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
A40: f3.p = 0 by FUNCT_1:49;
reconsider p1 = p as Point of TOP-REAL n1 by A4;
A41: 1 - |.p1.|*|.p1.| = 0 by A40,A39;
per cases;
suppose |.p1.| = 0; hence contradiction by A41; end;
suppose |.p1.| <> 0; then
|.p1.|*|.p1.| < 1*|.p1.| by Th5,XREAL_1:68;
hence contradiction by A41,Th5;
end;
end; then
consider f5 be Function of Tunit_ball n,R^1 such that
A42: (for p being Point of Tunit_ball n,r1 being Real st f4.p=r1
holds f5.p=1/r1) & f5 is continuous by JGRAPH_2:26;
consider f6 be Function of Tunit_ball n,TOP-REAL n such that
A43: (for a being Point of Tunit_ball n, b being Point of TOP-REAL n,
r being Real st a = b & f5.a = r holds f6.b = r*b) &
f6 is continuous by A42,Th2;
A44: dom f = the carrier of Tunit_ball(n) by FUNCT_2:def 1
.= dom f6 by FUNCT_2:def 1;
for x being object st x in dom f holds f.x = f6.x
proof
let x be object;
assume A45: x in dom f; then
reconsider p1 = x as Point of Tunit_ball n;
reconsider p = x as Point of TOP-REAL n by A45,A4;
f4.p = f3.p by A45,FUNCT_1:49
.= 1 - |.p.|*|.p.| by A39; then
f5.p1 = 1/(1 - |.p.|*|.p.|) by A42; then
f6.p1 = 1/(1 - |.p.|*|.p.|)*p by A43;
hence f.x = f6.x by A2;
end; then
A47: f = f6 by A44;
consider f8 be Function of TOP-REAL n,R^1 such that
A48: (for p being Point of TOP-REAL n,r1 being Real
st f2.p=r1 holds f8.p=4*r1) & f8 is continuous
by A37,JGRAPH_2:23;
consider f9 be Function of TOP-REAL n,R^1 such that
A49: (for p being Point of TOP-REAL n,r1,r2 being Real
st f0.p=r1 & f8.p=r2 holds f9.p=r1+r2) & f9 is continuous
by A48,A35,JGRAPH_2:19;
A50: 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 A49 .= 1 + f8.p by A35 .= 1 + 4*f2.p by A48
.= 1 + 4*(f1.p*f1.p) by A37 .= 1 + 4*(f1.p*|.p.|) by A36
.= 1 + 4*(|.p.|*|.p.|) by A36 .= 1 + 4*|.p.|*|.p.|;
end;
A51: for p being Point of TOP-REAL n ex r being Real 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 A50;
end;
consider f10 be Function of TOP-REAL n,R^1 such that
A52: (for p being Point of TOP-REAL n,r1 being Real
st f9.p=r1 holds f10.p=sqrt(r1)) & f10 is continuous
by A51,A49,JGRAPH_3:5;
consider f11 be Function of TOP-REAL n,R^1 such that
A53: (for p being Point of TOP-REAL n,r1,r2 being Real
st f0.p=r1 & f10.p=r2 holds f11.p=r1+r2) & f11 is continuous
by A52,A35,JGRAPH_2:19;
for p being Point of TOP-REAL n holds f11.p <> 0
proof
let p be Point of TOP-REAL n;
A54: f11.p = f0.p + f10.p by A53 .= 1 + f10.p by A35
.= 1 + sqrt(f9.p) by A52;
consider r be Real such that
A55: r = f9.p & r >= 0 by A51;
sqrt(f9.p) >= 0 by A55,SQUARE_1:def 2;
hence thesis by A54;
end; then
consider f12 be Function of TOP-REAL n,R^1 such that
A56: (for p being Point of TOP-REAL n,r1 being Real st f11.p=r1
holds f12.p=1/r1) & f12 is continuous by A53,JGRAPH_2:26;
consider f13 be Function of TOP-REAL n,R^1 such that
A57: (for p being Point of TOP-REAL n,r1 being Real
st f12.p=r1 holds f13.p=2*r1) & f13 is continuous
by A56,JGRAPH_2:23;
A58: 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 A57 .= 2*(1/f11.p) by A56
.= 2/(f0.p+f10.p) by A53
.= 2/(f0.p+sqrt(f9.p)) by A52
.= 2/(1+sqrt(f9.p)) by A35
.= 2/(1+sqrt(1 + 4*|.p.|*|.p.|)) by A50;
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
A59: (for a being Point of X, b being Point of TOP-REAL n,
r being Real st a = b & f13.a = r holds f14.b = r*b) &
f14 is continuous by A57,Th2;
reconsider f14 as continuous Function of TOP-REAL n, TOP-REAL n by A59;
A60: dom f14 = the carrier of TOP-REAL n by FUNCT_2:def 1;
A61: for r being Real holds |.r.|*|.r.| = r*r
proof
let r be Real;
per cases by ABSVALUE:1;
suppose |.r.| = r; hence thesis; end;
suppose |.r.| = -r; hence thesis; end;
end;
for y being object holds y in the carrier of Tunit_ball(n)
iff ex x being object st x in dom f14 & y = f14.x
proof
let y be object;
hereby
assume A62: y in the carrier of Tunit_ball(n);
[#] Tunit_ball(n) c= [#] TOP-REAL n by PRE_TOPC:def 4; then
reconsider q = y as Point of TOP-REAL n1 by A62;
|.q.| < 1 by A62,Th5; then
|.q.|*|.q.| <= 1*|.q.| by XREAL_1:64; then
|.q.|*|.q.| < 1 by A62,Th5,XXREAL_0:2; then
A63: 0 < 1 - |.q.|*|.q.| by XREAL_1:50;
set p = 1/(1-|.q.|*|.q.|)*q;
|.p.| = |.1/(1-|.q.|*|.q.|).|*|.q.| by TOPRNS_1:7; then
|.p.|*|.p.| = |.1/(1-|.q.|*|.q.|).|*|.1/(1-|.q.|*|.q.|).|*|.q.|*|.q.|
.= (1/(1-|.q.|*|.q.|))*(1/(1-|.q.|*|.q.|))*|.q.|*|.q.| by A61
.= (1*1)/((1-|.q.|*|.q.|)*(1-|.q.|*|.q.|))*|.q.|*|.q.| by XCMPLX_1:76
.= |.q.|*|.q.|/((1-|.q.|*|.q.|)*(1-|.q.|*|.q.|)); then
A64: 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 A63,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*|.p.|*|.p.|) = (1+|.q.|*|.q.|)/(1-|.q.|*|.q.|)
by A63,A64,SQUARE_1:22; then
A65: 1+sqrt(1 + 4*|.p.|*|.p.|)
= (1-|.q.|*|.q.|)/(1-|.q.|*|.q.|)+(1+|.q.|*|.q.|)/(1-|.q.|*|.q.|)
by A63,XCMPLX_1:60
.= 2/(1-|.q.|*|.q.|);
reconsider x = p as object;
take x;
thus x in dom f14 by A60;
thus f14.x = f13.p * p by A59
.= 2/(2/(1-|.q.|*|.q.|)) * p by A65,A58
.= (1-|.q.|*|.q.|) * p by XCMPLX_1:52
.= (1-|.q.|*|.q.|)/(1-|.q.|*|.q.|) * q by RLVECT_1:def 7
.= 1 * q by A63,XCMPLX_1:60
.= y by RLVECT_1:def 8;
end;
given x be object such that
A66: x in dom f14 & y = f14.x;
reconsider p = x as Point of TOP-REAL n1 by A66;
y in rng f14 by A66,FUNCT_1:3; then
reconsider q = y as Point of TOP-REAL n1;
y = (f13.p)*p by A59,A66
.= 2/(1+sqrt(1 + 4*|.p.|*|.p.|))*p by A58; then
|.q.| = |.2/(1+sqrt(1 + 4*|.p.|*|.p.|)).|*|.p.| by TOPRNS_1:7; then
A67: |.q.|*|.q.| = |.2/(1+sqrt(1 + 4*|.p.|*|.p.|)).|*
|.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 A61;
|.q.|*|.q.| < 1
proof
assume |.q.|*|.q.| >= 1; then
A68: ((2*2)/((1+sqrt(1 + 4*|.p.|*|.p.|))*(1+sqrt(1 + 4*|.p.|*|.p.|))))*
|.p.|*|.p.| >= 1 by A67,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 A68,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;
end; then
|.q.|^2 < 1; then
A69: |.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 A69,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);
end; then
A70: rng f14 = the carrier of Tunit_ball n by FUNCT_1:def 3; then
reconsider f14 as Function of TOP-REAL n, Tunit_ball n by A60,FUNCT_2:1;
A71: dom f14 = the carrier of TOP-REAL n by FUNCT_2:def 1
.= dom(f") by FUNCT_2:def 1;
for x being object st x in dom f14 holds f14.x = f".x
proof
let x be object;
assume A72: x in dom f14;
reconsider g = f as Function;
f is onto by A14,FUNCT_2:def 3;
then
A73: f" = g" by A34,TOPS_2:def 4;
A74: f14.x in rng f14 by A72,FUNCT_1:3; then
A75: f14.x in dom f by A70,FUNCT_2:def 1;
reconsider p = x as Point of TOP-REAL n1 by A72;
A76: f14.p = f13.p * p by A59 .= 2/(1+sqrt(1 + 4*|.p.|*|.p.|))*p by A58;
reconsider y = f14.x as Point of Tunit_ball(n) by A74;
reconsider q = y as Point of TOP-REAL n1 by A4;
A77: 0 <= sqrt(1 + 4*|.p.|*|.p.|) by SQUARE_1:def 2;
|.q.| = |.2/(1+sqrt(1 + 4*|.p.|*|.p.|)).|*|.p.| by A76,TOPRNS_1:7; then
|.q.|*|.q.| = |.2/(1+sqrt(1 + 4*|.p.|*|.p.|)).|*
|.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 A61
.= (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
A78: 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 A77,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 A77,XCMPLX_1:91;
f.(f14.x) = 1/(2/(1+sqrt(1 + 4*|.p.|*|.p.|))) * q by A2,A78
.= (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 A76,RLVECT_1:def 7
.= (2*(1+sqrt(1 + 4*|.p.|*|.p.|)))/(2*(1+sqrt(1 + 4*|.p.|*|.p.|)))*p
by XCMPLX_1:76
.= 1*p by A77,XCMPLX_1:60 .= p by RLVECT_1:def 8; then
[f14.x,x] in f by A75,FUNCT_1:def 2; then
[x,f14.x] in g~ by RELAT_1:def 7; then
[x,f14.x] in g" by A34,FUNCT_1:def 5;
hence f14.x = f".x by A73,FUNCT_1:1;
end; then
f" is continuous by A71,FUNCT_1:2,PRE_TOPC:27;
hence thesis by A3,A14,A34,A43,A47,TOPS_2:def 5;
end;
:: like TOPREALB:19
theorem
for r being positive Real,
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,
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 zero Element of NAT by A1,ORDINAL1:def 12;
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:62;
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
.= 1/r*p + (-1/r)*x by FUNCOP_1:7 .= 1/r*p - 1/r*x by RLVECT_1:79
.= 1/r*(p-x) by RLVECT_1:34 .= G.p by A6;
end; then
A8: G is continuous by TOPALG_1:16;
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 RLVECT_1:def 8
.= r*p + f2.p .= r*p + x by FUNCOP_1:7 .= F.p by A4;
end;
then
A11: F is continuous by TOPALG_1:16;
A12: the carrier of B = Ball(x,r) by MFOLD_0:2;
A13: the carrier of U = Ball(0.TOP-REAL n,1) by MFOLD_0:2;
A14: for a being object st a in dom f
holds f.a = (F|Ball(0.TOP-REAL n,1)).a
proof
let a be object such that
A15: a in dom f;
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;
end;
A16: 1/r*r = 1 by XCMPLX_1:87;
A17: rng f = [#]B
proof
now
let b be object;
assume A18: b in [#]B;
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: |.a-0.TOP-REAL n1.| = |.a.| by RLVECT_1:13
.= |.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,A12,A18,TOPREAL9:7; 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 RLVECT_1:def 7
.= c-x+x by A16,RLVECT_1:def 8 .= b by RLVECT_4:1;
hence b in rng f by A13,A10,A20,FUNCT_1:def 3;
end; then
[#]B c= rng f;
hence thesis by XBOOLE_0:def 10;
end;
now
let a, b be object 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,RLVECT_4:1;
hence a=b by RLVECT_1:36,RLVECT_4:1;
end; then
A25: f is one-to-one;
A26: for a being object st a in dom(f") holds f".a = (G|Ball(x,r)).a
proof
reconsider ff = f as Function;
let a be object such that
A27: a in dom (f");
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: |.e-0.TOP-REAL n1.| = |.e.| by RLVECT_1:13
.= |.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,A27,A12,TOPREAL9:7; then
A30: 1/r * (y - x) in Ball(0.TOP-REAL n,1) by A16,A29;
then f.e = r*e+x by A2,A13 .= r*(1/r)*(y-x)+x by RLVECT_1:def 7
.= y-x+x by A16,RLVECT_1:def 8 .= y by RLVECT_4:1;
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;
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 B by FUNCT_2:def 1;
f" is continuous by A32,A12,A7,A8,A26,BORSUK_4:44,FUNCT_1:2;
hence thesis by A9,A17,A25,A31,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 12;
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:25;
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, A1,Th6;
end;
suppose A4: n is empty;
A5: for x being object holds
x in Ball(0.TOP-REAL 0,1) iff x = 0.TOP-REAL 0
proof
let x be object;
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:39;
hence x in Ball(0.TOP-REAL 0,1);
end;
[#]TOP-REAL 0 = {0.TOP-REAL 0} by EUCLID:22,77
.= Ball(0.TOP-REAL 0,1) by A5,TARSKI:def 1;
hence thesis by A4,MFOLD_0:1;
end;
end;
reserve q for Point of TOP-REAL n;
::$CT
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 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 MFOLD_0:1;
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 MFOLD_0:3; then
B1, TOP-REAL n are_homeomorphic by A3,BORSUK_3:3;
:: 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,A2,BORSUK_3:3;
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 A0: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,A0, METRIZTS:def 1;
consider V be 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,A2,METRIZTS:3;
reconsider 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,PRE_TOPC:def 2; 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:7;
f .: U c= rng f by RELAT_1:111; then
A9: f .: U c= B by A4;
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;
end;
begin :: Manifold
reserve M for non empty TopSpace;
Lm1: (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)
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: 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;
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;
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;
consider f be Function of M|U1, (TOP-REAL n) | S such that
A5: f is being_homeomorphism by T_0TOPSP:def 1,A3,METRIZTS: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 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 be ball Subset of TOP-REAL n such that
A9: B c= S & q in B by A6,A7,Th3,FUNCT_2:5;
reconsider 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;
reconsider U2 = f" .: B1 as non empty Subset of M1 by A13;
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 as a_neighborhood of p by A19,CONNSP_2:3,9;
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 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;
end;
theorem Def4:
M is n-locally_euclidean without_boundary iff
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
proof
set TRn=TOP-REAL n;
hereby assume A1:M is n-locally_euclidean without_boundary;
let p be Point of M;
the carrier of M = Int M by A1,MFOLD_0:def 6;
:: then p in Int M;
then consider U be a_neighborhood of p,m be Nat such that
A2: M|U,Tball(0.TOP-REAL m,1) are_homeomorphic
by MFOLD_0:def 4;
set TR=TOP-REAL m;
consider W be a_neighborhood of p such that
A3: M|W,Tdisk(0.TRn,1) are_homeomorphic
by A1,MFOLD_0:def 3;
p in Int U & p in Int W by CONNSP_2:def 1;
then n=m by A2,A3,BROUWER3:15,XBOOLE_0:3;
hence ex U being a_neighborhood of p, S being open Subset of TRn
st U,S are_homeomorphic by A2,METRIZTS:def 1;
end;
assume R: for p being Point of M holds
ex U being a_neighborhood of p, S being open Subset of TRn
st U,S are_homeomorphic;
K: for p be Point of M
ex U be a_neighborhood of p st
M|U,Tball(0.TRn,1) are_homeomorphic
proof
let p be Point of M;
consider U be a_neighborhood of p, B be non empty ball Subset of TRn
such that
B1: U,B are_homeomorphic by R,Lm1;
take U;
consider q be Point of TRn, r be Real such that
B2: B = Ball(q,r) by Def1;
B3:M|U,TRn|Ball(q,r) are_homeomorphic by B1,B2,METRIZTS:def 1;
p in Int U by CONNSP_2:def 1;
then B4:ex W be Subset of M st W is open & W c= U & p in W by TOPS_1:22;
r>0 by B2;then
Tball(q,r),Tball(0.TRn,1) are_homeomorphic by MFOLD_0:3;
hence M|U,Tball(0.TRn,1) are_homeomorphic by B3,BORSUK_3:3,B4,B2;
end;
ZZ: now let p be Point of M;
ex U be a_neighborhood of p st
M|U,Tball(0.TOP-REAL n,1) are_homeomorphic by K;
hence ex U be a_neighborhood of p,n st
M|U,Tball(0.TOP-REAL n,1) are_homeomorphic;
end;
then F:M is without_boundary locally_euclidean by MFOLD_0:6;
for p being Point of M
ex U being a_neighborhood of p st
M|U,Tdisk(0.TOP-REAL n,1) are_homeomorphic
proof
let p be Point of M;
consider U be a_neighborhood of p,m be Nat such that
B1: M|U,Tdisk(0.TOP-REAL m,1) are_homeomorphic by MFOLD_0:def 2,F;
consider W be a_neighborhood of p such that
A3: M|W,Tball(0.TRn,1) are_homeomorphic
by K;
p in Int U & p in Int W by CONNSP_2:def 1;
:: then Int U meets Int W by XBOOLE_0:3;
then n=m by B1,A3,BROUWER3:15,XBOOLE_0:3;
hence thesis by B1;
end;
::then M is n-locally_euclidean by MFOLD_0:def 3;
hence thesis by ZZ,MFOLD_0:6,def 3;
end;
registration
let n;
cluster TOP-REAL n -> without_boundary n-locally_euclidean;
coherence
proof
now let p be Point of TOP-REAL n;
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,S;
thus U,S are_homeomorphic by METRIZTS:1;
end;
hence thesis by Def4;
end;
end;
:: Lemma 2.13a
theorem
M is without_boundary 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 M is without_boundary n-locally_euclidean;
then AA: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 by Def4;
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 AA,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 without_boundary n-locally_euclidean by Def4;
end;
:: Lemma 2.13b
theorem Th13:
M is without_boundary 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 M is without_boundary n-locally_euclidean;
then AA: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 by Def4;
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 Lm1,AA;
take U;
A3: (TOP-REAL n) | ([#]TOP-REAL n) = the TopStruct 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;
B1, the TopStruct of TOP-REAL n are_homeomorphic
by Th10,A3,METRIZTS:def 1;
hence U,[#]TOP-REAL n are_homeomorphic
by A3,METRIZTS:def 1,A4,BORSUK_3:3;
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;
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:93;
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:18;
reconsider S1 = (TOP-REAL n) | S as non empty TopSpace;
A11: the TopStruct of TOP-REAL n, S1 are_homeomorphic
by Th10,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 without_boundary n-locally_euclidean by Def4;
end;
registration
cluster without_boundary locally_euclidean ->
first-countable for non empty TopSpace;
correctness
proof
let M be non empty TopSpace;
assume A1: M is without_boundary 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,n such that
A2:M|U,Tball(0.TOP-REAL n,1) are_homeomorphic by A1,MFOLD_0:6;
set TR=TOP-REAL n;
p in Int U by CONNSP_2:def 1;
then K1:ex W be Subset of M st W is open & W c= U & p in W by TOPS_1:22;
Ball(0.TR,1) is non empty ball;
then Tball(0.TR,1),TR| ([#]TR) are_homeomorphic
by Th10,METRIZTS:def 1;
then M|U,TR| ([#]TR) are_homeomorphic by A2,K1,BORSUK_3:3;
then M|U, the TopStruct of TR are_homeomorphic by TSEP_1:93; then
consider f be Function of M|U, the TopStruct of TR such that
A3: f is being_homeomorphism by T_0TOPSP:def 1;
A4: dom f = [#](M|U) & rng f = [#](the TopStruct of TR) &
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 CONNSP_2:def 1,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;
consider B1 be 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 F(set) = f" .: $1 /\ Int U;
set B = {F(X) where X is Element of A: X in B1};
A11: card B1 c= omega by A10,CARD_3:def 14;
card B c= card B1 from TREES_2:sch 2; then
A12: card B c= omega by A11;
for x being object st x in B holds x in bool the carrier of M
proof
let x be object;
assume x in B; then
consider X1 be Element of A such that
A13: x = F(X1) & X1 in B1;
thus x in bool the carrier of M by A13;
end; then
reconsider B 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;
assume P in B; then
consider X1 be Element of A such that
A15: 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 in the topology of TOP-REAL n by PRE_TOPC:def 2,A15,YELLOW_8:12;
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 the TopStruct 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 be 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;
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
A21: Y = F(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;
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;
assume A24: S is open & p in S;
set S1 = S /\ [#](M|U);
S in the topology of M by A24,PRE_TOPC:def 2; then
A25: S1 in the topology of M|U by PRE_TOPC:def 4;
reconsider U1 = M|U as non empty TopStruct by A8,A7;
reconsider S1 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;
K: f .: S1 in the topology of the TopStruct of TOP-REAL n
by A26,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 be Subset of TOP-REAL n such that
A30: W in B1 & W c= S2 by A29,K,PRE_TOPC:def 2,YELLOW_8:13;
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 A30;
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;
hence V c= S by A33,A32,A34;
end; then
reconsider B as Basis of p by A14,A23,TOPS_2:def 1,YELLOW_8:def 1;
take B;
thus B is countable by A12,CARD_3:def 14;
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:93;
registration
cluster 0-locally_euclidean -> discrete for 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:16;
A5: p in U by A4, CONNSP_2:def 1;
consider f be Function of M|U, T such that
A6: f is being_homeomorphism by T_0TOPSP:def 1,A3,METRIZTS:def 1;
consider V be Subset of M such that
A7: V is open & V c= U & p in V by CONNSP_2:6;
for x being object holds x in V iff x = p
proof
let x be object;
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 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;
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:17;
end;
cluster discrete -> 0-locally_euclidean for non empty TopSpace;
coherence
proof
A14: [#]T = {0.TOP-REAL 0} by Lm2,EUCLID:22,77;
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:31;
A16: U is open & p in U by A15,TARSKI:def 1,TDLAT_3:15; then
reconsider U as a_neighborhood of p by CONNSP_2:3;
take U;
set f = {[p, 0.TOP-REAL 0]};
A17: p in [#](M|U) by A16,PRE_TOPC:def 5;
A19: dom f = U by RELAT_1:9; then
A20: dom f = [#](M|U) by PRE_TOPC:def 5;then
reconsider f as Function of M|U, T
by A17,Lm2,ZFMISC_1:87,FUNCT_2:def 1,ZFMISC_1:31;
A21: rng f = [#]T 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;
per cases;
suppose A22: P is empty;
thus thesis by A22;
end;
suppose A23: P is non empty; 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;
thus f.:P is closed implies P is closed by A23,A20,A19,ZFMISC_1:33;
end;
end; then
M|U, T are_homeomorphic by T_0TOPSP:def 1,A20,A21,TOPS_2:58;
hence U,[#]TOP-REAL 0 are_homeomorphic by METRIZTS:def 1;
end;
hence M is 0-locally_euclidean by Th13;
end;
end;
definition
let n, M;
attr M is n-manifold means
M is second-countable Hausdorff n-locally_euclidean;
end;
registration
let n;
cluster without_boundary n-manifold for non empty TopSpace;
existence
proof
take TOP-REAL n;
thus thesis;
end;
end;
registration
cluster second-countable discrete ->
0-locally_euclidean second-countable Hausdorff
for non empty TopSpace;
coherence;
end;
registration
let n;
cluster n-manifold ->
second-countable Hausdorff n-locally_euclidean for
non empty TopSpace;
correctness;
cluster second-countable Hausdorff n-locally_euclidean ->
n-manifold for non empty TopSpace;
correctness;
end;
:: Lemma 2.16
registration
let n;
let M be without_boundary n-manifold non empty TopSpace;
cluster open -> without_boundary n-manifold for 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 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: the TopStruct of X = the TopStruct of M|X1 by TSEP_1:5;
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;
consider f be Function of M|U2, (TOP-REAL n) | S2 such that
A11: f is being_homeomorphism by T_0TOPSP:def 1,A9,METRIZTS: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: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;
A13: (M|U2) | U3, ((TOP-REAL n) |S2 ) | (f.:U3) are_homeomorphic
by METRIZTS:def 1,A11,METRIZTS:3;
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
reconsider S = f.:U3 as open Subset of T2 by A14,PRE_TOPC:def 2;
S in the topology of T2 by PRE_TOPC:def 2; 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 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 as open Subset of TOP-REAL n by PRE_TOPC:def 2;
take U, S;
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: the TopStruct of X|U = the TopStruct 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;
end;
hence thesis by Def4;
end;
end;