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 Def3, 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;
A8:
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)
then reconsider hP =
h . p as
Point of
(TOP-REAL n) ;
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 r being
positive Real such that A16:
Ball (
hP,
r)
c= hib
by A15, TOPS_4:2;
|.(hP - hP).| = 0
by TOPRNS_1:28;
then A17:
hP in Ball (
hP,
r)
;
reconsider bb =
Ball (
hP,
r) as non
empty Subset of
(Tdisk ((0. (TOP-REAL n)),1)) by A16, 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, A8;
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;
rng h = [#] (Tdisk ((0. (TOP-REAL n)),1))
by A3, TOPS_2:def 5;
then A22:
h .: (h " bb) = bb
by FUNCT_1:77;
A24:
(Tdisk ((0. (TOP-REAL n)),1)) | bb = (TOP-REAL n) | (Ball (hP,r))
by A4, PRE_TOPC:7;
then reconsider hh =
h | (h " bb) as
Function of
(M | hb),
(Tball (hP,r)) by A19, JORDAN24:12, A22;
reconsider hb =
hb as
a_neighborhood of
p by A21, CONNSP_2:def 1;
hh is
being_homeomorphism
by A3, A19, A22, A24, METRIZTS:2;
then A25:
M | hb,
Tball (
hP,
r)
are_homeomorphic
by T_0TOPSP:def 1;
take hb =
hb;
M | hb, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
Tball (
hP,
r),
Tball (
(0. (TOP-REAL n)),1)
are_homeomorphic
by Th3;
hence
M | hb,
Tball (
(0. (TOP-REAL n)),1)
are_homeomorphic
by A25, BORSUK_3:3;
verum
end;
assume A26:
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 3 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 A27:
M | U,
Tball (
(0. (TOP-REAL n)),1)
are_homeomorphic
by A26;
A28:
n in NAT
by ORDINAL1:def 12;
A30:
[#] (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, A28;
set MU =
M | U;
consider h being
Function of
(M | U),
(Tball ((0. (TOP-REAL n)),1)) such that A31:
h is
being_homeomorphism
by A27, T_0TOPSP:def 1;
set En =
Euclid n;
A32:
Int U c= U
by TOPS_1:16;
A33:
[#] (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 A30, XBOOLE_1:1;
A34:
dom h = [#] (M | U)
by A31, TOPS_2:def 5;
then A35:
IU = h " hIU
by A31, FUNCT_1:82, FUNCT_1:76;
A36:
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)) ;
A37:
p in Int U
by CONNSP_2:def 1;
then A38:
h . p in hIU
by A34, 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 A38;
IU is
open
by TSEP_1:9;
then
h .: IU is
open
by A31, TOPGRP_1:25;
then
hIU is
open
by A30, TSEP_1:9;
then
hIU in the
topology of
(TOP-REAL n)
by PRE_TOPC:def 2;
then consider r being
Real such that A39:
r > 0
and A40:
Ball (
hp,
r)
c= hIUE
by A38, A36, PRE_TOPC:def 2, TOPMETR:15;
set r2 =
r / 2;
A41:
Ball (
Hp,
r)
= Ball (
hp,
r)
by TOPREAL9:13;
cl_Ball (
Hp,
(r / 2))
c= Ball (
Hp,
r)
by A28, XREAL_1:216, A39, JORDAN:21;
then A42:
cl_Ball (
Hp,
(r / 2))
c= hIU
by A40, A41;
then reconsider CL =
cl_Ball (
Hp,
(r / 2)) as
Subset of
(Tball ((0. (TOP-REAL n)),1)) by XBOOLE_1:1;
A43:
cl_Ball (
Hp,
(r / 2))
c= [#] (Tball ((0. (TOP-REAL n)),1))
by A42, XBOOLE_1:1;
then
cl_Ball (
Hp,
(r / 2))
c= rng h
by A31, TOPS_2:def 5;
then A44:
h .: (h " CL) = CL
by FUNCT_1:77;
set r22 =
(r / 2) / 2;
(r / 2) / 2
< r / 2
by A39, XREAL_1:216;
then A45:
Ball (
Hp,
((r / 2) / 2))
c= Ball (
Hp,
(r / 2))
by A28, JORDAN:18;
reconsider hCL =
h " CL as
Subset of
M by A33, XBOOLE_1:1;
A46:
(M | U) | (h " CL) = M | hCL
by A33, PRE_TOPC:7;
A47:
Ball (
Hp,
(r / 2))
c= cl_Ball (
Hp,
(r / 2))
by TOPREAL9:16;
then A48:
Ball (
Hp,
((r / 2) / 2))
c= cl_Ball (
Hp,
(r / 2))
by A45;
then reconsider BI =
Ball (
Hp,
((r / 2) / 2)) as
Subset of
(Tball ((0. (TOP-REAL n)),1)) by A43, XBOOLE_1:1;
BI c= hIU
by A42, A47, A45;
then A49:
h " BI c= h " hIU
by RELAT_1:143;
reconsider hBI =
h " BI as
Subset of
M by A33, XBOOLE_1:1;
BI is
open
by TSEP_1:9;
then
h " BI is
open
by A31, TOPGRP_1:26;
then A50:
hBI is
open
by A35, A49, TSEP_1:9;
|.(Hp - Hp).| = 0
by TOPRNS_1:28;
then
h . p in BI
by A39;
then
p in h " BI
by A37, A32, A33, A34, FUNCT_1:def 7;
then
p in Int hCL
by A48, RELAT_1:143, TOPS_1:22, A50;
then reconsider hCL =
hCL as
a_neighborhood of
p by CONNSP_2:def 1;
A51:
(Tball ((0. (TOP-REAL n)),1)) | CL = Tdisk (
Hp,
(r / 2))
by A30, PRE_TOPC:7;
then reconsider hh =
h | (h " CL) as
Function of
(M | hCL),
(Tdisk (Hp,(r / 2))) by A44, JORDAN24:12, A46;
hh is
being_homeomorphism
by A31, A51, METRIZTS:2, A44, A46;
then A52:
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, A39;
hence
ex
U being
a_neighborhood of
p st
M | U,
Tdisk (
(0. (TOP-REAL n)),1)
are_homeomorphic
by A52, BORSUK_3:3, A39;
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