let n be Nat; ( Tball ((0. (TOP-REAL n)),1) is n -locally_euclidean & Tball ((0. (TOP-REAL n)),1) is without_boundary )
set TR = TOP-REAL n;
set M = Tball ((0. (TOP-REAL n)),1);
A1:
for p being Point of (Tball ((0. (TOP-REAL n)),1)) ex U being a_neighborhood of p st (Tball ((0. (TOP-REAL n)),1)) | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
proof
let p be
Point of
(Tball ((0. (TOP-REAL n)),1));
ex U being a_neighborhood of p st (Tball ((0. (TOP-REAL n)),1)) | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
Int ([#] (Tball ((0. (TOP-REAL n)),1))) = [#] (Tball ((0. (TOP-REAL n)),1))
by TOPS_1:15;
then reconsider CM =
[#] (Tball ((0. (TOP-REAL n)),1)) as non
empty a_neighborhood of
p by CONNSP_2:def 1;
take
CM
;
(Tball ((0. (TOP-REAL n)),1)) | CM, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
thus
(Tball ((0. (TOP-REAL n)),1)) | CM,
Tball (
(0. (TOP-REAL n)),1)
are_homeomorphic
by TSEP_1:93;
verum
end;
A2:
for p being Point of (Tball ((0. (TOP-REAL n)),1)) ex U being a_neighborhood of p ex m being Nat st (Tball ((0. (TOP-REAL n)),1)) | U, Tball ((0. (TOP-REAL m)),1) are_homeomorphic
proof
let p be
Point of
(Tball ((0. (TOP-REAL n)),1));
ex U being a_neighborhood of p ex m being Nat st (Tball ((0. (TOP-REAL n)),1)) | U, Tball ((0. (TOP-REAL m)),1) are_homeomorphic
ex
U being
a_neighborhood of
p st
(Tball ((0. (TOP-REAL n)),1)) | U,
Tball (
(0. (TOP-REAL n)),1)
are_homeomorphic
by A1;
hence
ex
U being
a_neighborhood of
p ex
m being
Nat st
(Tball ((0. (TOP-REAL n)),1)) | U,
Tball (
(0. (TOP-REAL m)),1)
are_homeomorphic
;
verum
end;
then reconsider MM = Tball ((0. (TOP-REAL n)),1) as non empty locally_euclidean TopSpace by Lm2;
MM is n -locally_euclidean
proof
let p be
Point of
MM;
MFOLD_0:def 3 ex U being a_neighborhood of p st MM | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic
consider U being
a_neighborhood of
p such that A3:
MM | U,
Tball (
(0. (TOP-REAL n)),1)
are_homeomorphic
by A1;
A5:
p in Int U
by CONNSP_2:def 1;
consider W being
a_neighborhood of
p,
m being
Nat such that A6:
MM | W,
Tdisk (
(0. (TOP-REAL m)),1)
are_homeomorphic
by Def2;
p in Int W
by CONNSP_2:def 1;
then
m = n
by A5, XBOOLE_0:3, A3, A6, BROUWER3:15;
hence
ex
U being
a_neighborhood of
p st
MM | U,
Tdisk (
(0. (TOP-REAL n)),1)
are_homeomorphic
by A6;
verum
end;
hence
( Tball ((0. (TOP-REAL n)),1) is n -locally_euclidean & Tball ((0. (TOP-REAL n)),1) is without_boundary )
by A2, Lm2; verum