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, Def7;
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)) = 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, A11;
then A12:
Int hum = hum
by TOPS_1:23;
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 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 A14, A9, FUNCT_1:def 6;
then consider s being
Real such that A15:
s > 0
and A16:
Ball (
HQ,
s)
c= hum
by A12, 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 A3, TOPGRP_1:26;
hBB c= h " (h .: UIM)
by A16, A17, RELAT_1:143;
then A18:
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 A18, XBOOLE_1:1, A1;
hBBM is
open
by TSEP_1:9, A18;
then A19:
HBB is
open
by TSEP_1:9;
|.(hq - hq).| = 0
by TOPRNS_1:28;
then
hq in BB
by A15;
then
p in HBB
by FUNCT_1:def 7, A13, A4, A9, A7;
then A20:
p in Int HBB
by A19, TOPS_1:23;
A21:
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 A22:
(Tball ((0. (TOP-REAL n)),1)) | (h .: hBB) = (TOP-REAL n) | (Ball (hq,s))
by A11, PRE_TOPC:7;
reconsider HBB =
HBB as
a_neighborhood of
p by A20, 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 A3, A22, A23, A21, METRIZTS:2;
then A24:
(M | (Int M)) | HBB,
Tball (
hq,
s)
are_homeomorphic
by T_0TOPSP:def 1;
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 A15, Th3;
hence
(M | (Int M)) | HBB,
Tball (
(0. (TOP-REAL n)),1)
are_homeomorphic
by A15, A24, BORSUK_3:3;
verum
end;
hence
for b1 being non empty TopSpace st b1 = M | (Int M) holds
b1 is n -locally_euclidean
by Th13; verum