let n be Nat; :: thesis: for M being non empty TopSpace holds

( ( M is n -locally_euclidean & M is without_boundary ) iff for p being Point of M ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic )

let M be non empty TopSpace; :: thesis: ( ( M is n -locally_euclidean & M is without_boundary ) iff for p being Point of M ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic )

set TRn = TOP-REAL n;

K: for p being Point of M ex U being a_neighborhood of p st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic

for p being Point of M ex U being a_neighborhood of p st M | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic

( ( M is n -locally_euclidean & M is without_boundary ) iff for p being Point of M ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic )

let M be non empty TopSpace; :: thesis: ( ( M is n -locally_euclidean & M is without_boundary ) iff for p being Point of M ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic )

set TRn = TOP-REAL n;

hereby :: thesis: ( ( for p being Point of M ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic ) implies ( M is n -locally_euclidean & M is without_boundary ) )

assume R:
for p being Point of M ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic
; :: thesis: ( M is n -locally_euclidean & M is without_boundary )assume A1:
( M is n -locally_euclidean & M is without_boundary )
; :: thesis: for p being Point of M ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic

let p be Point of M; :: thesis: ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic

the carrier of M = Int M by A1, MFOLD_0:def 6;

then consider U being a_neighborhood of p, m being 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 being a_neighborhood of p such that

A3: M | W, Tdisk ((0. (TOP-REAL n)),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 ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic by A2, METRIZTS:def 1; :: thesis: verum

end;let p be Point of M; :: thesis: ex U being a_neighborhood of p ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic

the carrier of M = Int M by A1, MFOLD_0:def 6;

then consider U being a_neighborhood of p, m being 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 being a_neighborhood of p such that

A3: M | W, Tdisk ((0. (TOP-REAL n)),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 ex S being open Subset of (TOP-REAL n) st U,S are_homeomorphic by A2, METRIZTS:def 1; :: thesis: verum

K: for p being Point of M ex U being a_neighborhood of p st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic

proof

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

consider U being a_neighborhood of p, B being non empty ball Subset of (TOP-REAL n) such that

B1: U,B are_homeomorphic by R, Lm1;

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

consider q being Point of (TOP-REAL n), r being Real such that

B2: B = Ball (q,r) by Def1;

B3: M | U,(TOP-REAL n) | (Ball (q,r)) are_homeomorphic by B1, B2, METRIZTS:def 1;

p in Int U by CONNSP_2:def 1;

then B4: ex W being 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. (TOP-REAL n)),1) are_homeomorphic by MFOLD_0:3;

hence M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by B3, BORSUK_3:3, B4, B2; :: thesis: verum

end;consider U being a_neighborhood of p, B being non empty ball Subset of (TOP-REAL n) such that

B1: U,B are_homeomorphic by R, Lm1;

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

consider q being Point of (TOP-REAL n), r being Real such that

B2: B = Ball (q,r) by Def1;

B3: M | U,(TOP-REAL n) | (Ball (q,r)) are_homeomorphic by B1, B2, METRIZTS:def 1;

p in Int U by CONNSP_2:def 1;

then B4: ex W being 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. (TOP-REAL n)),1) are_homeomorphic by MFOLD_0:3;

hence M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by B3, BORSUK_3:3, B4, B2; :: thesis: verum

ZZ: now :: 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

then F:
( M is without_boundary & M is locally_euclidean )
by MFOLD_0:6;let p be Point of M; :: thesis: ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic

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

hence ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic ; :: thesis: verum

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

hence ex U being a_neighborhood of p ex n being Nat st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic ; :: thesis: verum

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

hence
( M is n -locally_euclidean & M is without_boundary )
by ZZ, MFOLD_0:6, MFOLD_0:def 3; :: thesis: verum
let p be Point of M; :: thesis: ex U being a_neighborhood of p st M | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic

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

B1: M | U, Tdisk ((0. (TOP-REAL m)),1) are_homeomorphic by MFOLD_0:def 2, F;

consider W being a_neighborhood of p such that

A3: M | W, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by K;

( p in Int U & p in Int W ) by CONNSP_2:def 1;

then n = m by B1, A3, BROUWER3:15, XBOOLE_0:3;

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

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

B1: M | U, Tdisk ((0. (TOP-REAL m)),1) are_homeomorphic by MFOLD_0:def 2, F;

consider W being a_neighborhood of p such that

A3: M | W, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by K;

( p in Int U & p in Int W ) by CONNSP_2:def 1;

then n = m by B1, A3, BROUWER3:15, XBOOLE_0:3;

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