let M be non empty locally_euclidean TopSpace; for p being Point of (M | (Int M)) ex U being a_neighborhood of p ex n being Nat st (M | (Int M)) | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
set MI = M | (Int M);
let p be Point of (M | (Int M)); ex U being a_neighborhood of p ex n being Nat st (M | (Int M)) | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
A1:
[#] (M | (Int M)) = Int M
by PRE_TOPC:def 5;
then
p in Int M
;
then reconsider q = p as Point of M ;
consider U being a_neighborhood of q, n being Nat such that
A2:
M | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
by A1, Def4;
A3:
Int U c= U
by TOPS_1:16;
A4:
(Int M) /\ (Int U) in the topology of M
by PRE_TOPC:def 2;
A5:
Int U c= U
by TOPS_1:16;
set MU = M | U;
set TR = TOP-REAL n;
consider h being Function of (M | U),(Tball ((0. (TOP-REAL n)),1)) such that
A6:
h is being_homeomorphism
by A2, T_0TOPSP:def 1;
A7:
[#] (M | U) = U
by PRE_TOPC:def 5;
(Int U) /\ (Int M) c= Int U
by XBOOLE_1:17;
then reconsider UIM = (Int M) /\ (Int U) as Subset of (M | U) by A5, A7, XBOOLE_1:1;
A8:
dom h = [#] (M | U)
by A6, TOPS_2:def 5;
A10:
[#] (Tball ((0. (TOP-REAL n)),1)) = Ball ((0. (TOP-REAL n)),1)
by PRE_TOPC:def 5;
then reconsider hum = h .: UIM as Subset of (TOP-REAL n) by XBOOLE_1:1;
UIM /\ ([#] (M | U)) = UIM
by XBOOLE_1:28;
then
UIM in the topology of (M | U)
by A4, PRE_TOPC:def 4;
then
UIM is open
by PRE_TOPC:def 2;
then
h .: UIM is open
by A6, TOPGRP_1:25;
then
hum is open
by TSEP_1:9, A10;
then A11:
Int hum = hum
by TOPS_1:23;
A12:
h " (h .: UIM) c= UIM
by A6, FUNCT_1:82;
A13:
q in Int U
by CONNSP_2:def 1;
then A14:
q in UIM
by A1, XBOOLE_0:def 4;
then
h . q in hum
by A8, FUNCT_1:def 6;
then reconsider hq = h . q as Point of (TOP-REAL n) ;
reconsider HQ = hq as Point of (Euclid n) by EUCLID:67;
h . q in h .: UIM
by A14, A8, FUNCT_1:def 6;
then consider s being Real such that
A15:
s > 0
and
A16:
Ball (HQ,s) c= hum
by A11, GOBOARD6:5;
A17:
Ball (HQ,s) = Ball (hq,s)
by TOPREAL9:13;
then reconsider BB = Ball (hq,s) as Subset of (Tball ((0. (TOP-REAL n)),1)) by A16, XBOOLE_1:1;
BB is open
by TSEP_1:9;
then reconsider hBB = h " BB as open Subset of (M | U) by A6, TOPGRP_1:26;
hBB c= h " (h .: UIM)
by A16, A17, RELAT_1:143;
then A18:
hBB c= UIM
by A12;
reconsider hBBM = hBB as Subset of M by A7, XBOOLE_1:1;
(Int U) /\ (Int M) c= Int M
by XBOOLE_1:17;
then reconsider HBB = hBBM as Subset of (M | (Int M)) by A18, XBOOLE_1:1, A1;
hBBM is open
by TSEP_1:9, A18;
then A19:
HBB is open
by TSEP_1:9;
A20:
M | hBBM = (M | (Int M)) | HBB
by A1, PRE_TOPC:7;
rng h = [#] (Tball ((0. (TOP-REAL n)),1))
by A6, TOPS_2:def 5;
then
h .: hBB = BB
by FUNCT_1:77;
then A21:
(Tball ((0. (TOP-REAL n)),1)) | (h .: hBB) = (TOP-REAL n) | (Ball (hq,s))
by A10, PRE_TOPC:7;
|.(hq - hq).| = 0
by TOPRNS_1:28;
then
hq in BB
by A15;
then
p in HBB
by FUNCT_1:def 7, A13, A3, A8, A7;
then
p in Int HBB
by A19, TOPS_1:23;
then reconsider HBB = HBB as a_neighborhood of p by CONNSP_2:def 1;
A22:
(M | U) | hBB = M | hBBM
by A7, PRE_TOPC:7;
then reconsider hh = h | hBB as Function of ((M | (Int M)) | HBB),((TOP-REAL n) | (Ball (hq,s))) by A21, JORDAN24:12, A20;
hh is being_homeomorphism
by A6, A21, A22, A20, METRIZTS:2;
then A23:
(M | (Int M)) | HBB, Tball (hq,s) are_homeomorphic
by T_0TOPSP:def 1;
take
HBB
; ex n being Nat st (M | (Int M)) | HBB, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
Tball (hq,s), Tball ((0. (TOP-REAL n)),1) are_homeomorphic
by A15, Th3;
hence
ex n being Nat st (M | (Int M)) | HBB, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
by A15, A23, BORSUK_3:3; verum