let n be Nat; 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; ( ( 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 ( ( 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 A1:
(
M is
n -locally_euclidean &
M is
without_boundary )
;
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;
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;
verum
end;
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
; ( M is n -locally_euclidean & M is without_boundary )
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;
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
;
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;
verum
end;
then F:
( M is without_boundary & M is 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;
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;
verum
end;
hence
( M is n -locally_euclidean & M is without_boundary )
by ZZ, MFOLD_0:6, MFOLD_0:def 3; verum