let M be non empty TopSpace; :: thesis: ( ( M is locally_euclidean & M is without_boundary ) iff for p being Point of M ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic )

thus M is locally_euclidean :: thesis: M is without_boundary

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of M or x in Int M )

assume x in the carrier of M ; :: thesis: x in Int M

then reconsider p = x as Point of M ;

ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A27;

hence x in Int M by Def4; :: thesis: verum

hereby :: thesis: ( ( for p being Point of M ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic ) implies ( M is locally_euclidean & M is without_boundary ) )

assume A27:
for p being Point of M ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
; :: thesis: ( M is locally_euclidean & M is without_boundary )assume A1:
( M is locally_euclidean & M is without_boundary )
; :: thesis: for p being Point of M ex hb being a_neighborhood of p ex n being Nat st M | hb, Tball ((0. (TOP-REAL n)),1) are_homeomorphic

let p be Point of M; :: thesis: ex hb being a_neighborhood of p ex n being Nat st M | hb, Tball ((0. (TOP-REAL n)),1) are_homeomorphic

consider U being a_neighborhood of p, n being Nat such that

A2: M | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by A1;

set MU = M | U;

set TR = TOP-REAL n;

consider h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) such that

A3: h is being_homeomorphism by A2, T_0TOPSP:def 1;

A4: cl_Ball ((0. (TOP-REAL n)),1) = (Ball ((0. (TOP-REAL n)),1)) \/ (Sphere ((0. (TOP-REAL n)),1)) by TOPREAL9:18;

A5: [#] (Tdisk ((0. (TOP-REAL n)),1)) = cl_Ball ((0. (TOP-REAL n)),1) by PRE_TOPC:def 5;

then reconsider B = Ball ((0. (TOP-REAL n)),1) as Subset of (Tdisk ((0. (TOP-REAL n)),1)) by TOPREAL9:16;

A6: [#] (M | U) = U by PRE_TOPC:def 5;

then reconsider IU = Int U as Subset of (M | U) by TOPS_1:16;

A7: p in Int U by CONNSP_2:def 1;

reconsider B = B as open Subset of (Tdisk ((0. (TOP-REAL n)),1)) by TSEP_1:9;

set HIB = B /\ (h .: (Int U));

reconsider hib = B /\ (h .: (Int U)) as Subset of (TOP-REAL n) by A5, XBOOLE_1:1;

A8: B /\ (h .: (Int U)) c= Ball ((0. (TOP-REAL n)),1) by XBOOLE_1:17;

IU is open by TSEP_1:9;

then h .: (Int U) is open by A3, TOPGRP_1:25;

then A9: hib is open by TSEP_1:9, A8;

reconsider MM = M as non empty locally_euclidean TopSpace by A1;

A10: Int U c= U by TOPS_1:16;

A11: dom h = [#] (M | U) by A3, TOPS_2:def 5;

then A12: h . p in rng h by A7, A10, A6, FUNCT_1:def 3;

A13: h . p in Ball ((0. (TOP-REAL n)),1)

h . p in h .: (Int U) by A7, A10, A6, A11, FUNCT_1:def 6;

then h . p in hib by A13, XBOOLE_0:def 4;

then consider r being positive Real such that

A15: Ball (hP,r) c= hib by A9, TOPS_4:2;

|.(hP - hP).| = 0 by TOPRNS_1:28;

then A16: hP in Ball (hP,r) ;

reconsider bb = Ball (hP,r) as non empty Subset of (Tdisk ((0. (TOP-REAL n)),1)) by A15, XBOOLE_1:1;

reconsider hb = h " bb as Subset of M by A6, XBOOLE_1:1;

bb is open by TSEP_1:9;

then A17: h " bb is open by A3, TOPGRP_1:26;

A18: h " (B /\ (h .: (Int U))) c= h " (h .: (Int U)) by XBOOLE_1:17, RELAT_1:143;

A19: h " (h .: (Int U)) c= Int U by A3, FUNCT_1:82;

A20: M | hb = (M | U) | (h " bb) by A6, PRE_TOPC:7;

hb c= h " (B /\ (h .: (Int U))) by A15, RELAT_1:143;

then hb c= Int U by A18, A19;

then A21: hb is open by A6, TSEP_1:9, A17, A10;

p in hb by A16, A7, A10, A6, A11, FUNCT_1:def 7;

then A22: p in Int hb by A21, TOPS_1:23;

rng h = [#] (Tdisk ((0. (TOP-REAL n)),1)) by A3, TOPS_2:def 5;

then A23: h .: (h " bb) = bb by FUNCT_1:77;

A25: (Tdisk ((0. (TOP-REAL n)),1)) | bb = (TOP-REAL n) | (Ball (hP,r)) by A5, PRE_TOPC:7;

then reconsider hh = h | (h " bb) as Function of (M | hb),(Tball (hP,r)) by A20, JORDAN24:12, A23;

reconsider hb = hb as a_neighborhood of p by A22, CONNSP_2:def 1;

hh is being_homeomorphism by A3, A20, A23, A25, METRIZTS:2;

then A26: M | hb, Tball (hP,r) are_homeomorphic by T_0TOPSP:def 1;

take hb = hb; :: thesis: ex n being Nat st M | hb, Tball ((0. (TOP-REAL n)),1) are_homeomorphic

take n = n; :: thesis: M | hb, Tball ((0. (TOP-REAL n)),1) are_homeomorphic

Tball (hP,r), Tball ((0. (TOP-REAL n)),1) are_homeomorphic by Th3;

hence M | hb, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A26, BORSUK_3:3; :: thesis: verum

end;let p be Point of M; :: thesis: ex hb being a_neighborhood of p ex n being Nat st M | hb, Tball ((0. (TOP-REAL n)),1) are_homeomorphic

consider U being a_neighborhood of p, n being Nat such that

A2: M | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by A1;

set MU = M | U;

set TR = TOP-REAL n;

consider h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) such that

A3: h is being_homeomorphism by A2, T_0TOPSP:def 1;

A4: cl_Ball ((0. (TOP-REAL n)),1) = (Ball ((0. (TOP-REAL n)),1)) \/ (Sphere ((0. (TOP-REAL n)),1)) by TOPREAL9:18;

A5: [#] (Tdisk ((0. (TOP-REAL n)),1)) = cl_Ball ((0. (TOP-REAL n)),1) by PRE_TOPC:def 5;

then reconsider B = Ball ((0. (TOP-REAL n)),1) as Subset of (Tdisk ((0. (TOP-REAL n)),1)) by TOPREAL9:16;

A6: [#] (M | U) = U by PRE_TOPC:def 5;

then reconsider IU = Int U as Subset of (M | U) by TOPS_1:16;

A7: p in Int U by CONNSP_2:def 1;

reconsider B = B as open Subset of (Tdisk ((0. (TOP-REAL n)),1)) by TSEP_1:9;

set HIB = B /\ (h .: (Int U));

reconsider hib = B /\ (h .: (Int U)) as Subset of (TOP-REAL n) by A5, XBOOLE_1:1;

A8: B /\ (h .: (Int U)) c= Ball ((0. (TOP-REAL n)),1) by XBOOLE_1:17;

IU is open by TSEP_1:9;

then h .: (Int U) is open by A3, TOPGRP_1:25;

then A9: hib is open by TSEP_1:9, A8;

reconsider MM = M as non empty locally_euclidean TopSpace by A1;

A10: Int U c= U by TOPS_1:16;

A11: dom h = [#] (M | U) by A3, TOPS_2:def 5;

then A12: h . p in rng h by A7, A10, A6, FUNCT_1:def 3;

A13: h . p in Ball ((0. (TOP-REAL n)),1)

proof

then reconsider hP = h . p as Point of (TOP-REAL n) ;
assume
not h . p in Ball ((0. (TOP-REAL n)),1)
; :: thesis: contradiction

then A14: h . p in Sphere ((0. (TOP-REAL n)),1) by A5, A12, A4, XBOOLE_0:def 3;

Fr MM = the carrier of MM \ (Int MM) by SUBSET_1:def 4

.= {} by XBOOLE_1:37, A1 ;

hence contradiction by A14, A3, Th5; :: thesis: verum

end;then A14: h . p in Sphere ((0. (TOP-REAL n)),1) by A5, A12, A4, XBOOLE_0:def 3;

Fr MM = the carrier of MM \ (Int MM) by SUBSET_1:def 4

.= {} by XBOOLE_1:37, A1 ;

hence contradiction by A14, A3, Th5; :: thesis: verum

h . p in h .: (Int U) by A7, A10, A6, A11, FUNCT_1:def 6;

then h . p in hib by A13, XBOOLE_0:def 4;

then consider r being positive Real such that

A15: Ball (hP,r) c= hib by A9, TOPS_4:2;

|.(hP - hP).| = 0 by TOPRNS_1:28;

then A16: hP in Ball (hP,r) ;

reconsider bb = Ball (hP,r) as non empty Subset of (Tdisk ((0. (TOP-REAL n)),1)) by A15, XBOOLE_1:1;

reconsider hb = h " bb as Subset of M by A6, XBOOLE_1:1;

bb is open by TSEP_1:9;

then A17: h " bb is open by A3, TOPGRP_1:26;

A18: h " (B /\ (h .: (Int U))) c= h " (h .: (Int U)) by XBOOLE_1:17, RELAT_1:143;

A19: h " (h .: (Int U)) c= Int U by A3, FUNCT_1:82;

A20: M | hb = (M | U) | (h " bb) by A6, PRE_TOPC:7;

hb c= h " (B /\ (h .: (Int U))) by A15, RELAT_1:143;

then hb c= Int U by A18, A19;

then A21: hb is open by A6, TSEP_1:9, A17, A10;

p in hb by A16, A7, A10, A6, A11, FUNCT_1:def 7;

then A22: p in Int hb by A21, TOPS_1:23;

rng h = [#] (Tdisk ((0. (TOP-REAL n)),1)) by A3, TOPS_2:def 5;

then A23: h .: (h " bb) = bb by FUNCT_1:77;

A25: (Tdisk ((0. (TOP-REAL n)),1)) | bb = (TOP-REAL n) | (Ball (hP,r)) by A5, PRE_TOPC:7;

then reconsider hh = h | (h " bb) as Function of (M | hb),(Tball (hP,r)) by A20, JORDAN24:12, A23;

reconsider hb = hb as a_neighborhood of p by A22, CONNSP_2:def 1;

hh is being_homeomorphism by A3, A20, A23, A25, METRIZTS:2;

then A26: M | hb, Tball (hP,r) are_homeomorphic by T_0TOPSP:def 1;

take hb = hb; :: thesis: ex n being Nat st M | hb, Tball ((0. (TOP-REAL n)),1) are_homeomorphic

take n = n; :: thesis: M | hb, Tball ((0. (TOP-REAL n)),1) are_homeomorphic

Tball (hP,r), Tball ((0. (TOP-REAL n)),1) are_homeomorphic by Th3;

hence M | hb, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A26, BORSUK_3:3; :: thesis: verum

thus M is locally_euclidean :: thesis: M is without_boundary

proof

thus
Int M c= the carrier of M
; :: according to XBOOLE_0:def 10,MFOLD_0:def 6 :: thesis: the carrier of M c= Int M
let p be Point of M; :: according to MFOLD_0:def 2 :: thesis: ex U being a_neighborhood of p ex n being Nat st M | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic

consider U being a_neighborhood of p, n being Nat such that

A28: M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A27;

set En = Euclid n;

set TR = TOP-REAL n;

A29: Int U c= U by TOPS_1:16;

[#] (Tdisk ((0. (TOP-REAL n)),1)) = cl_Ball ((0. (TOP-REAL n)),1) by PRE_TOPC:def 5;

then reconsider B = Ball ((0. (TOP-REAL n)),1) as Subset of (Tdisk ((0. (TOP-REAL n)),1)) by TOPREAL9:16;

set MU = M | U;

consider h being Function of (M | U),(Tball ((0. (TOP-REAL n)),1)) such that

A30: h is being_homeomorphism by A28, T_0TOPSP:def 1;

A31: n in NAT by ORDINAL1:def 12;

A33: [#] (Tball ((0. (TOP-REAL n)),1)) = Ball ((0. (TOP-REAL n)),1) by PRE_TOPC:def 5;

then reconsider clB = cl_Ball ((0. (TOP-REAL n)),(1 / 2)) as non empty Subset of (Tball ((0. (TOP-REAL n)),1)) by JORDAN:21, A31;

A34: [#] (M | U) = U by PRE_TOPC:def 5;

then reconsider IU = Int U as Subset of (M | U) by TOPS_1:16;

reconsider hIU = h .: IU as Subset of (TOP-REAL n) by A33, XBOOLE_1:1;

A35: dom h = [#] (M | U) by A30, TOPS_2:def 5;

then A36: IU = h " hIU by A30, FUNCT_1:82, FUNCT_1:76;

A37: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;

then reconsider hIUE = hIU as Subset of (TopSpaceMetr (Euclid n)) ;

A38: p in Int U by CONNSP_2:def 1;

then A39: h . p in hIU by A35, FUNCT_1:def 6;

then reconsider hp = h . p as Point of (Euclid n) by EUCLID:67;

reconsider Hp = h . p as Point of (TOP-REAL n) by A39;

IU is open by TSEP_1:9;

then h .: IU is open by A30, TOPGRP_1:25;

then hIU is open by A33, TSEP_1:9;

then hIU in the topology of (TOP-REAL n) by PRE_TOPC:def 2;

then consider r being Real such that

A40: r > 0 and

A41: Ball (hp,r) c= hIUE by A39, A37, PRE_TOPC:def 2, TOPMETR:15;

set r2 = r / 2;

A42: Ball (Hp,r) = Ball (hp,r) by TOPREAL9:13;

cl_Ball (Hp,(r / 2)) c= Ball (Hp,r) by A31, XREAL_1:216, A40, JORDAN:21;

then A43: cl_Ball (Hp,(r / 2)) c= hIU by A41, A42;

then reconsider CL = cl_Ball (Hp,(r / 2)) as Subset of (Tball ((0. (TOP-REAL n)),1)) by XBOOLE_1:1;

A44: cl_Ball (Hp,(r / 2)) c= [#] (Tball ((0. (TOP-REAL n)),1)) by A43, XBOOLE_1:1;

then cl_Ball (Hp,(r / 2)) c= rng h by A30, TOPS_2:def 5;

then A45: h .: (h " CL) = CL by FUNCT_1:77;

set r22 = (r / 2) / 2;

(r / 2) / 2 < r / 2 by A40, XREAL_1:216;

then A46: Ball (Hp,((r / 2) / 2)) c= Ball (Hp,(r / 2)) by A31, JORDAN:18;

reconsider hCL = h " CL as Subset of M by A34, XBOOLE_1:1;

A47: (M | U) | (h " CL) = M | hCL by A34, PRE_TOPC:7;

A48: Ball (Hp,(r / 2)) c= cl_Ball (Hp,(r / 2)) by TOPREAL9:16;

then A49: Ball (Hp,((r / 2) / 2)) c= cl_Ball (Hp,(r / 2)) by A46;

then reconsider BI = Ball (Hp,((r / 2) / 2)) as Subset of (Tball ((0. (TOP-REAL n)),1)) by A44, XBOOLE_1:1;

BI c= hIU by A43, A48, A46;

then A50: h " BI c= h " hIU by RELAT_1:143;

reconsider hBI = h " BI as Subset of M by A34, XBOOLE_1:1;

BI is open by TSEP_1:9;

then h " BI is open by A30, TOPGRP_1:26;

then A51: hBI is open by A36, A50, TSEP_1:9;

|.(Hp - Hp).| = 0 by TOPRNS_1:28;

then h . p in BI by A40;

then p in h " BI by A38, A29, A34, A35, FUNCT_1:def 7;

then p in Int hCL by A49, RELAT_1:143, TOPS_1:22, A51;

then reconsider hCL = hCL as a_neighborhood of p by CONNSP_2:def 1;

A52: (Tball ((0. (TOP-REAL n)),1)) | CL = Tdisk (Hp,(r / 2)) by A33, PRE_TOPC:7;

then reconsider hh = h | (h " CL) as Function of (M | hCL),(Tdisk (Hp,(r / 2))) by A45, JORDAN24:12, A47;

hh is being_homeomorphism by A30, A52, METRIZTS:2, A45, A47;

then A53: M | hCL, Tdisk (Hp,(r / 2)) are_homeomorphic by T_0TOPSP:def 1;

Tdisk (Hp,(r / 2)), Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by Lm1, A40;

hence ex U being a_neighborhood of p ex n being Nat st M | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by A53, BORSUK_3:3, A40; :: thesis: verum

end;consider U being a_neighborhood of p, n being Nat such that

A28: M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A27;

set En = Euclid n;

set TR = TOP-REAL n;

A29: Int U c= U by TOPS_1:16;

[#] (Tdisk ((0. (TOP-REAL n)),1)) = cl_Ball ((0. (TOP-REAL n)),1) by PRE_TOPC:def 5;

then reconsider B = Ball ((0. (TOP-REAL n)),1) as Subset of (Tdisk ((0. (TOP-REAL n)),1)) by TOPREAL9:16;

set MU = M | U;

consider h being Function of (M | U),(Tball ((0. (TOP-REAL n)),1)) such that

A30: h is being_homeomorphism by A28, T_0TOPSP:def 1;

A31: n in NAT by ORDINAL1:def 12;

A33: [#] (Tball ((0. (TOP-REAL n)),1)) = Ball ((0. (TOP-REAL n)),1) by PRE_TOPC:def 5;

then reconsider clB = cl_Ball ((0. (TOP-REAL n)),(1 / 2)) as non empty Subset of (Tball ((0. (TOP-REAL n)),1)) by JORDAN:21, A31;

A34: [#] (M | U) = U by PRE_TOPC:def 5;

then reconsider IU = Int U as Subset of (M | U) by TOPS_1:16;

reconsider hIU = h .: IU as Subset of (TOP-REAL n) by A33, XBOOLE_1:1;

A35: dom h = [#] (M | U) by A30, TOPS_2:def 5;

then A36: IU = h " hIU by A30, FUNCT_1:82, FUNCT_1:76;

A37: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;

then reconsider hIUE = hIU as Subset of (TopSpaceMetr (Euclid n)) ;

A38: p in Int U by CONNSP_2:def 1;

then A39: h . p in hIU by A35, FUNCT_1:def 6;

then reconsider hp = h . p as Point of (Euclid n) by EUCLID:67;

reconsider Hp = h . p as Point of (TOP-REAL n) by A39;

IU is open by TSEP_1:9;

then h .: IU is open by A30, TOPGRP_1:25;

then hIU is open by A33, TSEP_1:9;

then hIU in the topology of (TOP-REAL n) by PRE_TOPC:def 2;

then consider r being Real such that

A40: r > 0 and

A41: Ball (hp,r) c= hIUE by A39, A37, PRE_TOPC:def 2, TOPMETR:15;

set r2 = r / 2;

A42: Ball (Hp,r) = Ball (hp,r) by TOPREAL9:13;

cl_Ball (Hp,(r / 2)) c= Ball (Hp,r) by A31, XREAL_1:216, A40, JORDAN:21;

then A43: cl_Ball (Hp,(r / 2)) c= hIU by A41, A42;

then reconsider CL = cl_Ball (Hp,(r / 2)) as Subset of (Tball ((0. (TOP-REAL n)),1)) by XBOOLE_1:1;

A44: cl_Ball (Hp,(r / 2)) c= [#] (Tball ((0. (TOP-REAL n)),1)) by A43, XBOOLE_1:1;

then cl_Ball (Hp,(r / 2)) c= rng h by A30, TOPS_2:def 5;

then A45: h .: (h " CL) = CL by FUNCT_1:77;

set r22 = (r / 2) / 2;

(r / 2) / 2 < r / 2 by A40, XREAL_1:216;

then A46: Ball (Hp,((r / 2) / 2)) c= Ball (Hp,(r / 2)) by A31, JORDAN:18;

reconsider hCL = h " CL as Subset of M by A34, XBOOLE_1:1;

A47: (M | U) | (h " CL) = M | hCL by A34, PRE_TOPC:7;

A48: Ball (Hp,(r / 2)) c= cl_Ball (Hp,(r / 2)) by TOPREAL9:16;

then A49: Ball (Hp,((r / 2) / 2)) c= cl_Ball (Hp,(r / 2)) by A46;

then reconsider BI = Ball (Hp,((r / 2) / 2)) as Subset of (Tball ((0. (TOP-REAL n)),1)) by A44, XBOOLE_1:1;

BI c= hIU by A43, A48, A46;

then A50: h " BI c= h " hIU by RELAT_1:143;

reconsider hBI = h " BI as Subset of M by A34, XBOOLE_1:1;

BI is open by TSEP_1:9;

then h " BI is open by A30, TOPGRP_1:26;

then A51: hBI is open by A36, A50, TSEP_1:9;

|.(Hp - Hp).| = 0 by TOPRNS_1:28;

then h . p in BI by A40;

then p in h " BI by A38, A29, A34, A35, FUNCT_1:def 7;

then p in Int hCL by A49, RELAT_1:143, TOPS_1:22, A51;

then reconsider hCL = hCL as a_neighborhood of p by CONNSP_2:def 1;

A52: (Tball ((0. (TOP-REAL n)),1)) | CL = Tdisk (Hp,(r / 2)) by A33, PRE_TOPC:7;

then reconsider hh = h | (h " CL) as Function of (M | hCL),(Tdisk (Hp,(r / 2))) by A45, JORDAN24:12, A47;

hh is being_homeomorphism by A30, A52, METRIZTS:2, A45, A47;

then A53: M | hCL, Tdisk (Hp,(r / 2)) are_homeomorphic by T_0TOPSP:def 1;

Tdisk (Hp,(r / 2)), Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by Lm1, A40;

hence ex U being a_neighborhood of p ex n being Nat st M | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by A53, BORSUK_3:3, A40; :: thesis: verum

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of M or x in Int M )

assume x in the carrier of M ; :: thesis: x in Int M

then reconsider p = x as Point of M ;

ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A27;

hence x in Int M by Def4; :: thesis: verum