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