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. ()),1) are_homeomorphic )
hereby :: thesis: ( ( for p being Point of M ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. ()),1) are_homeomorphic ) implies ( 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. ()),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. ()),1) are_homeomorphic
consider U being a_neighborhood of p, n being Nat such that
A2: M | U, Tdisk ((0. ()),1) are_homeomorphic by A1;
set MU = M | U;
set TR = TOP-REAL n;
consider h being Function of (M | U),(Tdisk ((0. ()),1)) such that
A3: h is being_homeomorphism by ;
A4: cl_Ball ((0. ()),1) = (Ball ((0. ()),1)) \/ (Sphere ((0. ()),1)) by TOPREAL9:18;
A5: [#] (Tdisk ((0. ()),1)) = cl_Ball ((0. ()),1) by PRE_TOPC:def 5;
then reconsider B = Ball ((0. ()),1) as Subset of (Tdisk ((0. ()),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. ()),1)) by TSEP_1:9;
set HIB = B /\ (h .: (Int U));
reconsider hib = B /\ (h .: (Int U)) as Subset of () by ;
A8: B /\ (h .: (Int U)) c= Ball ((0. ()),1) by XBOOLE_1:17;
IU is open by TSEP_1:9;
then h .: (Int U) is open by ;
then A9: hib is open by ;
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 ;
then A12: h . p in rng h by ;
A13: h . p in Ball ((0. ()),1)
proof
assume not h . p in Ball ((0. ()),1) ; :: thesis: contradiction
then A14: h . p in Sphere ((0. ()),1) by ;
Fr MM = the carrier of MM \ (Int MM) by SUBSET_1:def 4
.= {} by ;
hence contradiction by A14, A3, Th5; :: thesis: verum
end;
then reconsider hP = h . p as Point of () ;
h . p in h .: (Int U) by ;
then h . p in hib by ;
then consider r being positive Real such that
A15: Ball (hP,r) c= hib by ;
|.(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. ()),1)) by ;
reconsider hb = h " bb as Subset of M by ;
bb is open by TSEP_1:9;
then A17: h " bb is open by ;
A18: h " (B /\ (h .: (Int U))) c= h " (h .: (Int U)) by ;
A19: h " (h .: (Int U)) c= Int U by ;
A20: M | hb = (M | U) | (h " bb) by ;
hb c= h " (B /\ (h .: (Int U))) by ;
then hb c= Int U by ;
then A21: hb is open by ;
p in hb by ;
then A22: p in Int hb by ;
rng h = [#] (Tdisk ((0. ()),1)) by ;
then A23: h .: (h " bb) = bb by FUNCT_1:77;
A25: (Tdisk ((0. ()),1)) | bb = () | (Ball (hP,r)) by ;
then reconsider hh = h | (h " bb) as Function of (M | hb),(Tball (hP,r)) by ;
reconsider hb = hb as a_neighborhood of p by ;
hh is being_homeomorphism by ;
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. ()),1) are_homeomorphic
take n = n; :: thesis: M | hb, Tball ((0. ()),1) are_homeomorphic
Tball (hP,r), Tball ((0. ()),1) are_homeomorphic by Th3;
hence M | hb, Tball ((0. ()),1) are_homeomorphic by ; :: thesis: verum
end;
assume A27: for p being Point of M ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. ()),1) are_homeomorphic ; :: thesis: ( M is locally_euclidean & M is without_boundary )
thus M is locally_euclidean :: thesis:
proof
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. ()),1) are_homeomorphic
consider U being a_neighborhood of p, n being Nat such that
A28: M | U, Tball ((0. ()),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. ()),1)) = cl_Ball ((0. ()),1) by PRE_TOPC:def 5;
then reconsider B = Ball ((0. ()),1) as Subset of (Tdisk ((0. ()),1)) by TOPREAL9:16;
set MU = M | U;
consider h being Function of (M | U),(Tball ((0. ()),1)) such that
A30: h is being_homeomorphism by ;
A31: n in NAT by ORDINAL1:def 12;
A33: [#] (Tball ((0. ()),1)) = Ball ((0. ()),1) by PRE_TOPC:def 5;
then reconsider clB = cl_Ball ((0. ()),(1 / 2)) as non empty Subset of (Tball ((0. ()),1)) by ;
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 () by ;
A35: dom h = [#] (M | U) by ;
then A36: IU = h " hIU by ;
A37: TopStruct(# the carrier of (), the topology of () #) = TopSpaceMetr () by EUCLID:def 8;
then reconsider hIUE = hIU as Subset of () ;
A38: p in Int U by CONNSP_2:def 1;
then A39: h . p in hIU by ;
then reconsider hp = h . p as Point of () by EUCLID:67;
reconsider Hp = h . p as Point of () by A39;
IU is open by TSEP_1:9;
then h .: IU is open by ;
then hIU is open by ;
then hIU in the topology of () by PRE_TOPC:def 2;
then consider r being Real such that
A40: r > 0 and
A41: Ball (hp,r) c= hIUE by ;
set r2 = r / 2;
A42: Ball (Hp,r) = Ball (hp,r) by TOPREAL9:13;
cl_Ball (Hp,(r / 2)) c= Ball (Hp,r) by ;
then A43: cl_Ball (Hp,(r / 2)) c= hIU by ;
then reconsider CL = cl_Ball (Hp,(r / 2)) as Subset of (Tball ((0. ()),1)) by XBOOLE_1:1;
A44: cl_Ball (Hp,(r / 2)) c= [#] (Tball ((0. ()),1)) by ;
then cl_Ball (Hp,(r / 2)) c= rng h by ;
then A45: h .: (h " CL) = CL by FUNCT_1:77;
set r22 = (r / 2) / 2;
(r / 2) / 2 < r / 2 by ;
then A46: Ball (Hp,((r / 2) / 2)) c= Ball (Hp,(r / 2)) by ;
reconsider hCL = h " CL as Subset of M by ;
A47: (M | U) | (h " CL) = M | hCL by ;
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. ()),1)) by ;
BI c= hIU by ;
then A50: h " BI c= h " hIU by RELAT_1:143;
reconsider hBI = h " BI as Subset of M by ;
BI is open by TSEP_1:9;
then h " BI is open by ;
then A51: hBI is open by ;
|.(Hp - Hp).| = 0 by TOPRNS_1:28;
then h . p in BI by A40;
then p in h " BI by ;
then p in Int hCL by ;
then reconsider hCL = hCL as a_neighborhood of p by CONNSP_2:def 1;
A52: (Tball ((0. ()),1)) | CL = Tdisk (Hp,(r / 2)) by ;
then reconsider hh = h | (h " CL) as Function of (M | hCL),(Tdisk (Hp,(r / 2))) by ;
hh is being_homeomorphism by ;
then A53: M | hCL, Tdisk (Hp,(r / 2)) are_homeomorphic by T_0TOPSP:def 1;
Tdisk (Hp,(r / 2)), Tdisk ((0. ()),1) are_homeomorphic by ;
hence ex U being a_neighborhood of p ex n being Nat st M | U, Tdisk ((0. ()),1) are_homeomorphic by ; :: thesis: verum
end;
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 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. ()),1) are_homeomorphic by A27;
hence x in Int M by Def4; :: thesis: verum