let M be non empty locally_euclidean TopSpace; :: thesis: 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)); :: thesis: 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, Def3;
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) = (TOP-REAL n) | (Ball ((0. (TOP-REAL n)),1)) by MFOLD_1:def 2;
then A11: [#] (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, A11;
then A12: Int hum = hum by TOPS_1:23;
A13: h " (h .: UIM) c= UIM by A6, FUNCT_1:82;
A14: q in Int U by CONNSP_2:def 1;
then A15: 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 A15, A8, FUNCT_1:def 6;
then consider s being Real such that
A16: s > 0 and
A17: Ball (HQ,s) c= hum by A12, GOBOARD6:5;
A18: 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 A17, 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 A17, A18, RELAT_1:143;
then A19: hBB c= UIM by A13;
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 A19, XBOOLE_1:1, A1;
hBBM is open by TSEP_1:9, A19;
then A20: HBB is open by TSEP_1:9;
A21: 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 A22: (Tball ((0. (TOP-REAL n)),1)) | (h .: hBB) = (TOP-REAL n) | (Ball (hq,s)) by A10, A11, PRE_TOPC:7;
|.(hq - hq).| = 0 by TOPRNS_1:28;
then hq in BB by A16;
then p in HBB by FUNCT_1:def 7, A14, A3, A8, A7;
then p in Int HBB by A20, TOPS_1:23;
then reconsider HBB = HBB as a_neighborhood of p by CONNSP_2:def 1;
A23: (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 A22, JORDAN24:12, A21;
hh is being_homeomorphism by A6, A22, A23, A21, METRIZTS:2;
then (M | (Int M)) | HBB,(TOP-REAL n) | (Ball (hq,s)) are_homeomorphic by T_0TOPSP:def 1;
then A24: (M | (Int M)) | HBB, Tball (hq,s) are_homeomorphic by MFOLD_1:def 2;
take HBB ; :: thesis: 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 A16, MFOLD_1:9;
hence ex n being Nat st (M | (Int M)) | HBB, Tball ((0. (TOP-REAL n)),1) are_homeomorphic by A16, A24, BORSUK_3:3; :: thesis: verum