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