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