let n be Nat; for M being non empty TopSpace holds
( M is non empty n -locally_euclidean without_boundary TopSpace iff for p being Point of M ex U being a_neighborhood of p st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic )
let M be non empty TopSpace; ( M is non empty n -locally_euclidean without_boundary TopSpace iff for p being Point of M ex U being a_neighborhood of p st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic )
set TR = TOP-REAL n;
hereby ( ( for p being Point of M ex U being a_neighborhood of p st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic ) implies M is non empty n -locally_euclidean without_boundary TopSpace )
assume A1:
M is non
empty n -locally_euclidean without_boundary TopSpace
;
for p being Point of M ex hb being a_neighborhood of p st M | hb, Tball ((0. (TOP-REAL n)),1) are_homeomorphic then reconsider MM =
M as non
empty n -locally_euclidean without_boundary TopSpace ;
let p be
Point of
M;
ex hb being a_neighborhood of p st M | hb, Tball ((0. (TOP-REAL n)),1) are_homeomorphic consider U being
a_neighborhood of
p such that A2:
M | U,
Tdisk (
(0. (TOP-REAL n)),1)
are_homeomorphic
by Def2, A1;
set MU =
M | U;
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:
[#] (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;
reconsider B =
B as
open Subset of
(Tdisk ((0. (TOP-REAL n)),1)) by TSEP_1:9;
A5:
Int U c= U
by TOPS_1:16;
set HIB =
B /\ (h .: (Int U));
reconsider hib =
B /\ (h .: (Int U)) as
Subset of
(TOP-REAL n) by A4, XBOOLE_1:1;
A6:
B /\ (h .: (Int U)) c= Ball (
(0. (TOP-REAL n)),1)
by XBOOLE_1:17;
A7:
h " (B /\ (h .: (Int U))) c= h " (h .: (Int U))
by XBOOLE_1:17, RELAT_1:143;
AA:
h " (h .: (Int U)) c= Int U
by A3, FUNCT_1:82;
A9:
cl_Ball (
(0. (TOP-REAL n)),1)
= (Ball ((0. (TOP-REAL n)),1)) \/ (Sphere ((0. (TOP-REAL n)),1))
by TOPREAL9:18;
A10:
[#] (M | U) = U
by PRE_TOPC:def 5;
then reconsider IU =
Int U as
Subset of
(M | U) by TOPS_1:16;
A11:
p in Int U
by CONNSP_2:def 1;
A12:
dom h = [#] (M | U)
by A3, TOPS_2:def 5;
then A13:
h . p in rng h
by A11, A5, A10, FUNCT_1:def 3;
A14:
h . p in Ball (
(0. (TOP-REAL n)),1)
IU is
open
by TSEP_1:9;
then
h .: (Int U) is
open
by A3, TOPGRP_1:25;
then A15:
hib is
open
by TSEP_1:9, A6;
h . p in h .: (Int U)
by A11, A5, A10, A12, FUNCT_1:def 6;
then
h . p in hib
by A14, XBOOLE_0:def 4;
then consider BB being
ball Subset of
(TOP-REAL n) such that A16:
BB c= hib
and A17:
h . p in BB
by A15, MFOLD_1:3;
reconsider bb =
BB as non
empty Subset of
(Tdisk ((0. (TOP-REAL n)),1)) by A16, A17, XBOOLE_1:1;
reconsider hb =
h " bb as
Subset of
M by A10, XBOOLE_1:1;
bb is
open
by TSEP_1:9;
then A18:
h " bb is
open
by A3, TOPGRP_1:26;
A19:
M | hb = (M | U) | (h " bb)
by A10, PRE_TOPC:7;
hb c= h " (B /\ (h .: (Int U)))
by A16, RELAT_1:143;
then
hb c= Int U
by A7, AA;
then A20:
hb is
open
by A10, TSEP_1:9, A18, A5;
p in hb
by A17, A11, A5, A10, A12, FUNCT_1:def 7;
then A21:
p in Int hb
by A20, TOPS_1:23;
consider q being
Point of
(TOP-REAL n),
r being
Real such that A22:
BB = Ball (
q,
r)
by MFOLD_1:def 1;
rng h = [#] (Tdisk ((0. (TOP-REAL n)),1))
by A3, TOPS_2:def 5;
then A23:
h .: (h " bb) = bb
by FUNCT_1:77;
A24:
(TOP-REAL n) | (Ball (q,r)) = Tball (
q,
r)
by MFOLD_1:def 2;
A25:
(Tdisk ((0. (TOP-REAL n)),1)) | bb = (TOP-REAL n) | (Ball (q,r))
by A4, A22, PRE_TOPC:7;
then reconsider hh =
h | (h " bb) as
Function of
(M | hb),
(Tball (q,r)) by A19, JORDAN24:12, A23, A24;
reconsider hb =
hb as
a_neighborhood of
p by A21, CONNSP_2:def 1;
hh is
being_homeomorphism
by A3, A19, A23, A24, A25, METRIZTS:2;
then A26:
M | hb,
Tball (
q,
r)
are_homeomorphic
by T_0TOPSP:def 1;
take hb =
hb;
M | hb, Tball ((0. (TOP-REAL n)),1) are_homeomorphic A27:
r > 0
by A17, A22;
then
Tball (
q,
r),
Tball (
(0. (TOP-REAL n)),1)
are_homeomorphic
by MFOLD_1:9;
hence
M | hb,
Tball (
(0. (TOP-REAL n)),1)
are_homeomorphic
by A26, BORSUK_3:3, A27;
verum
end;
assume A28:
for p being Point of M ex U being a_neighborhood of p st M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
; M is non empty n -locally_euclidean without_boundary TopSpace
M is n -locally_euclidean
proof
[#] (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;
reconsider B =
B as
open Subset of
(Tdisk ((0. (TOP-REAL n)),1)) by TSEP_1:9;
let p be
Point of
M;
MFOLD_0:def 2 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 such that A29:
M | U,
Tball (
(0. (TOP-REAL n)),1)
are_homeomorphic
by A28;
N:
n in NAT
by ORDINAL1:def 12;
A30:
Tball (
(0. (TOP-REAL n)),1)
= (TOP-REAL n) | (Ball ((0. (TOP-REAL n)),1))
by MFOLD_1:def 2;
then A31:
[#] (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, N;
set MU =
M | U;
consider h being
Function of
(M | U),
(Tball ((0. (TOP-REAL n)),1)) such that A32:
h is
being_homeomorphism
by A29, T_0TOPSP:def 1;
set En =
Euclid n;
A33:
Int U c= U
by TOPS_1:16;
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 A31, XBOOLE_1:1;
A36:
dom h = [#] (M | U)
by A32, TOPS_2:def 5;
then A37:
IU = h " hIU
by A32, FUNCT_1:82, FUNCT_1:76;
A38:
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)) ;
A39:
p in Int U
by CONNSP_2:def 1;
then A40:
h . p in hIU
by A36, 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 A40;
IU is
open
by TSEP_1:9;
then
h .: IU is
open
by A32, TOPGRP_1:25;
then
hIU is
open
by A31, TSEP_1:9;
then
hIU in the
topology of
(TOP-REAL n)
by PRE_TOPC:def 2;
then consider r being
Real such that A41:
r > 0
and A42:
Ball (
hp,
r)
c= hIUE
by A40, A38, PRE_TOPC:def 2, TOPMETR:15;
set r2 =
r / 2;
A43:
Ball (
Hp,
r)
= Ball (
hp,
r)
by TOPREAL9:13;
cl_Ball (
Hp,
(r / 2))
c= Ball (
Hp,
r)
by N, XREAL_1:216, A41, JORDAN:21;
then A44:
cl_Ball (
Hp,
(r / 2))
c= hIU
by A42, A43;
then reconsider CL =
cl_Ball (
Hp,
(r / 2)) as
Subset of
(Tball ((0. (TOP-REAL n)),1)) by XBOOLE_1:1;
A45:
cl_Ball (
Hp,
(r / 2))
c= [#] (Tball ((0. (TOP-REAL n)),1))
by A44, XBOOLE_1:1;
then
cl_Ball (
Hp,
(r / 2))
c= rng h
by A32, TOPS_2:def 5;
then A46:
h .: (h " CL) = CL
by FUNCT_1:77;
set r22 =
(r / 2) / 2;
(r / 2) / 2
< r / 2
by A41, XREAL_1:216;
then A47:
Ball (
Hp,
((r / 2) / 2))
c= Ball (
Hp,
(r / 2))
by N, JORDAN:18;
reconsider hCL =
h " CL as
Subset of
M by A34, XBOOLE_1:1;
A48:
(M | U) | (h " CL) = M | hCL
by A34, PRE_TOPC:7;
A49:
Ball (
Hp,
(r / 2))
c= cl_Ball (
Hp,
(r / 2))
by TOPREAL9:16;
then A50:
Ball (
Hp,
((r / 2) / 2))
c= cl_Ball (
Hp,
(r / 2))
by A47;
then reconsider BI =
Ball (
Hp,
((r / 2) / 2)) as
Subset of
(Tball ((0. (TOP-REAL n)),1)) by A45, XBOOLE_1:1;
BI c= hIU
by A44, A49, A47;
then A51:
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 A32, TOPGRP_1:26;
then A52:
hBI is
open
by A37, A51, TSEP_1:9;
|.(Hp - Hp).| = 0
by TOPRNS_1:28;
then
h . p in BI
by A41;
then
p in h " BI
by A39, A33, A34, A36, FUNCT_1:def 7;
then
p in Int hCL
by A50, RELAT_1:143, TOPS_1:22, A52;
then reconsider hCL =
hCL as
a_neighborhood of
p by CONNSP_2:def 1;
A53:
(Tball ((0. (TOP-REAL n)),1)) | CL = Tdisk (
Hp,
(r / 2))
by A30, A31, PRE_TOPC:7;
then reconsider hh =
h | (h " CL) as
Function of
(M | hCL),
(Tdisk (Hp,(r / 2))) by A46, JORDAN24:12, A48;
hh is
being_homeomorphism
by A32, A53, METRIZTS:2, A46, A48;
then A54:
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, A41;
hence
ex
U being
a_neighborhood of
p st
M | U,
Tdisk (
(0. (TOP-REAL n)),1)
are_homeomorphic
by A54, BORSUK_3:3, A41;
verum
end;
then reconsider M = M as non empty n -locally_euclidean TopSpace ;
M is without_boundary
hence
M is non empty n -locally_euclidean without_boundary TopSpace
; verum