let M be non empty locally_euclidean with_boundary TopSpace; for p being Point of M
for n being Nat st ex U being a_neighborhood of p st M | U, Tdisk ((0. (TOP-REAL (n + 1))),1) are_homeomorphic holds
for pF being Point of (M | (Fr M)) st p = pF holds
ex U being a_neighborhood of pF st (M | (Fr M)) | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
let p be Point of M; for n being Nat st ex U being a_neighborhood of p st M | U, Tdisk ((0. (TOP-REAL (n + 1))),1) are_homeomorphic holds
for pF being Point of (M | (Fr M)) st p = pF holds
ex U being a_neighborhood of pF st (M | (Fr M)) | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
let n be Nat; ( ex U being a_neighborhood of p st M | U, Tdisk ((0. (TOP-REAL (n + 1))),1) are_homeomorphic implies for pF being Point of (M | (Fr M)) st p = pF holds
ex U being a_neighborhood of pF st (M | (Fr M)) | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic )
assume A1:
ex U being a_neighborhood of p st M | U, Tdisk ((0. (TOP-REAL (n + 1))),1) are_homeomorphic
; for pF being Point of (M | (Fr M)) st p = pF holds
ex U being a_neighborhood of pF st (M | (Fr M)) | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
set n1 = n + 1;
set TR = TOP-REAL (n + 1);
consider W being a_neighborhood of p such that
A2:
M | W, Tdisk ((0. (TOP-REAL (n + 1))),1) are_homeomorphic
by A1;
A3:
p in Int W
by CONNSP_2:def 1;
set TR1 = TOP-REAL n;
set CL = cl_Ball ((0. (TOP-REAL (n + 1))),1);
set S = Sphere ((0. (TOP-REAL (n + 1))),1);
set F = Fr M;
set MF = M | (Fr M);
let pF be Point of (M | (Fr M)); ( p = pF implies ex U being a_neighborhood of pF st (M | (Fr M)) | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic )
assume A4:
p = pF
; ex U being a_neighborhood of pF st (M | (Fr M)) | U, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
A5:
[#] (M | (Fr M)) = Fr M
by PRE_TOPC:def 5;
then consider U being a_neighborhood of p, m being Nat, h being Function of (M | U),(Tdisk ((0. (TOP-REAL m)),1)) such that
A6:
h is being_homeomorphism
and
A7:
h . p in Sphere ((0. (TOP-REAL m)),1)
by A4, Th3;
A8:
p in Int U
by CONNSP_2:def 1;
M | U, Tdisk ((0. (TOP-REAL m)),1) are_homeomorphic
by A6, T_0TOPSP:def 1;
then A9:
m = n + 1
by A3, A8, XBOOLE_0:3, A2, BROUWER3:14;
then reconsider h = h as Function of (M | U),(Tdisk ((0. (TOP-REAL (n + 1))),1)) ;
A10:
Int U c= U
by TOPS_1:16;
[#] (M | U) = U
by PRE_TOPC:def 5;
then reconsider IU = Int U as Subset of (M | U) by TOPS_1:16;
set MU = M | U;
A11:
pF in Int U
by A4, CONNSP_2:def 1;
then
p in (Fr M) /\ IU
by A4, A5, XBOOLE_0:def 4;
then reconsider FIU = (Fr M) /\ (Int U) as non empty Subset of (M | U) ;
A12:
[#] (M | U) = U
by PRE_TOPC:def 5;
IU is open
by TSEP_1:9;
then
h .: IU is open
by A9, A6, TOPGRP_1:25;
then
h .: IU in the topology of (Tdisk ((0. (TOP-REAL (n + 1))),1))
by PRE_TOPC:def 2;
then consider W being Subset of (TOP-REAL (n + 1)) such that
A13:
W in the topology of (TOP-REAL (n + 1))
and
A14:
h .: IU = W /\ ([#] (Tdisk ((0. (TOP-REAL (n + 1))),1)))
by PRE_TOPC:def 4;
reconsider W = W as open Subset of (TOP-REAL (n + 1)) by A13, PRE_TOPC:def 2;
A15:
h .: IU = W /\ (cl_Ball ((0. (TOP-REAL (n + 1))),1))
by PRE_TOPC:def 5, A14;
A16:
dom h = [#] (M | U)
by A6, TOPS_2:def 5;
then A17:
h . p in h .: IU
by A4, A11, FUNCT_1:def 6;
then reconsider hp = h . p as Point of (TOP-REAL (n + 1)) by A15;
A18:
Int W = W
by TOPS_1:23;
A19:
|.(hp - (0. (TOP-REAL (n + 1)))).| = 1
by A9, A7, TOPREAL9:9;
reconsider HP = hp as Point of (Euclid (n + 1)) by EUCLID:67;
h . p in W
by A17, A14, XBOOLE_0:def 4;
then consider s being Real such that
A20:
s > 0
and
A21:
Ball (HP,s) c= W
by A18, GOBOARD6:5;
set s2 = s / 2;
set m = min ((s / 2),(1 / 2));
set V0 = (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2)))));
set hV0 = h " ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2))))));
A22:
min ((s / 2),(1 / 2)) <= s / 2
by XXREAL_0:17;
s / 2 < s
by A20, XREAL_1:216;
then A23:
Ball (hp,(min ((s / 2),(1 / 2)))) c= Ball (hp,s)
by A22, XXREAL_0:2, JORDAN:18;
A24:
Ball (HP,s) = Ball (hp,s)
by TOPREAL9:13;
A25:
h " ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2)))))) c= Fr M
proof
let x be
object ;
TARSKI:def 3 ( not x in h " ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2)))))) or x in Fr M )
assume A26:
x in h " ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2))))))
;
x in Fr M
then A27:
h . x in (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2)))))
by FUNCT_1:def 7;
A28:
x in dom h
by A26, FUNCT_1:def 7;
then reconsider q =
x as
Point of
M by A16, A12;
reconsider hq =
h . q as
Point of
(TOP-REAL (n + 1)) by A27;
h . q in Ball (
hp,
(min ((s / 2),(1 / 2))))
by A27, XBOOLE_0:def 4;
then A29:
h . q in Ball (
hp,
s)
by A23;
A30:
h . q in Sphere (
(0. (TOP-REAL (n + 1))),1)
by A27, XBOOLE_0:def 4;
then
|.(hq - (0. (TOP-REAL (n + 1)))).| = 1
by TOPREAL9:9;
then
hq in cl_Ball (
(0. (TOP-REAL (n + 1))),1)
;
then
h . q in h .: IU
by A15, A29, A21, A24, XBOOLE_0:def 4;
then consider y being
object such that A31:
y in dom h
and A32:
y in IU
and A33:
h . y = h . q
by FUNCT_1:def 6;
y = q
by A6, A31, A33, A28, FUNCT_1:def 4;
then
U is
a_neighborhood of
q
by A32, CONNSP_2:def 1;
hence
x in Fr M
by A9, A6, Th3, A30;
verum
end;
reconsider FIU1 = FIU as Subset of (M | (Fr M)) by XBOOLE_1:17, A5;
Int U in the topology of M
by PRE_TOPC:def 2;
then
FIU1 in the topology of (M | (Fr M))
by A5, PRE_TOPC:def 4;
then A34:
FIU1 is open
by PRE_TOPC:def 2;
A35:
(M | (Fr M)) | FIU1 = M | ((Fr M) /\ (Int U))
by XBOOLE_1:17, PRE_TOPC:7;
set Mfiu = (M | U) | FIU;
A36:
(Fr M) /\ U c= U
by XBOOLE_1:17;
A38:
[#] ((TOP-REAL (n + 1)) | (cl_Ball ((0. (TOP-REAL (n + 1))),1))) = cl_Ball ((0. (TOP-REAL (n + 1))),1)
by PRE_TOPC:def 5;
then reconsider hFIU = h .: FIU as Subset of (TOP-REAL (n + 1)) by XBOOLE_1:1;
A39:
[#] ((TOP-REAL (n + 1)) | hFIU) = hFIU
by PRE_TOPC:def 5;
A40:
(Tdisk ((0. (TOP-REAL (n + 1))),1)) | (h .: FIU) = (TOP-REAL (n + 1)) | hFIU
by A38, PRE_TOPC:7;
then reconsider hfiu = h | FIU as Function of ((M | U) | FIU),((TOP-REAL (n + 1)) | hFIU) by JORDAN24:12;
A41:
hfiu is being_homeomorphism
by A9, A6, METRIZTS:2, A40;
A42:
Ball ((0. (TOP-REAL n)),1) misses Sphere ((0. (TOP-REAL n)),1)
by TOPREAL9:19;
A43:
Sphere ((0. (TOP-REAL (n + 1))),1) c= cl_Ball ((0. (TOP-REAL (n + 1))),1)
by TOPREAL9:17;
A44:
IU = h " (h .: IU)
by FUNCT_1:82, A6, FUNCT_1:76, A16;
(Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2))))) c= Ball (hp,(min ((s / 2),(1 / 2))))
by XBOOLE_1:17;
then A45:
(Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2))))) c= W
by A21, A23, A24;
BB:
(Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2))))) c= hFIU
proof
let x be
object ;
TARSKI:def 3 ( not x in (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2))))) or x in hFIU )
assume A46:
x in (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2)))))
;
x in hFIU
then reconsider q =
x as
Point of
(TOP-REAL (n + 1)) ;
q in Sphere (
(0. (TOP-REAL (n + 1))),1)
by A46, XBOOLE_0:def 4;
then
q in h .: IU
by A45, A46, A15, A43, XBOOLE_0:def 4;
then consider w being
object such that A47:
w in dom h
and A48:
w in IU
and A49:
h . w = q
by FUNCT_1:def 6;
reconsider w =
w as
Point of
(M | U) by A47;
w in h " ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2))))))
by A46, A47, A49, FUNCT_1:def 7;
then
w in FIU
by A25, A48, XBOOLE_0:def 4;
hence
x in hFIU
by A47, A49, FUNCT_1:def 6;
verum
end;
A51:
(Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2))))) c= Sphere ((0. (TOP-REAL (n + 1))),1)
by XBOOLE_1:17;
then
(Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2))))) c= cl_Ball ((0. (TOP-REAL (n + 1))),1)
by A43;
then
(Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2))))) c= h .: IU
by A45, A14, XBOOLE_1:19, A38;
then A52:
h " ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2)))))) c= IU
by A44, RELAT_1:143;
A53:
rng h = [#] (Tdisk ((0. (TOP-REAL (n + 1))),1))
by A9, A6, TOPS_2:def 5;
then
h .: (h " ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2))))))) = (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2)))))
by FUNCT_1:77, A43, A51, XBOOLE_1:1, A38;
then A54:
(Tdisk ((0. (TOP-REAL (n + 1))),1)) | (h .: (h " ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2)))))))) = (TOP-REAL (n + 1)) | ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2))))))
by PRE_TOPC:7, A43, A51, XBOOLE_1:1;
A55:
cl_Ball ((0. (TOP-REAL (n + 1))),1) = (Sphere ((0. (TOP-REAL (n + 1))),1)) \/ (Ball ((0. (TOP-REAL (n + 1))),1))
by TOPREAL9:18;
A56:
hFIU /\ (Ball (hp,(min ((s / 2),(1 / 2))))) c= (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2)))))
proof
let x be
object ;
TARSKI:def 3 ( not x in hFIU /\ (Ball (hp,(min ((s / 2),(1 / 2))))) or x in (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2))))) )
assume A57:
x in hFIU /\ (Ball (hp,(min ((s / 2),(1 / 2)))))
;
x in (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2)))))
then reconsider q =
x as
Point of
(TOP-REAL (n + 1)) ;
A58:
x in hFIU
by A57, XBOOLE_0:def 4;
A59:
q in Sphere (
(0. (TOP-REAL (n + 1))),1)
proof
reconsider Q =
q as
Point of
(Euclid (n + 1)) by EUCLID:67;
set WB =
W /\ (Ball ((0. (TOP-REAL (n + 1))),1));
A60:
Int (W /\ (Ball ((0. (TOP-REAL (n + 1))),1))) = W /\ (Ball ((0. (TOP-REAL (n + 1))),1))
by TOPS_1:23;
hFIU c= h .: IU
by XBOOLE_1:17, RELAT_1:123;
then A61:
q in W
by A58, A14, XBOOLE_0:def 4;
assume
not
q in Sphere (
(0. (TOP-REAL (n + 1))),1)
;
contradiction
then
q in Ball (
(0. (TOP-REAL (n + 1))),1)
by A58, A38, A55, XBOOLE_0:def 3;
then
q in W /\ (Ball ((0. (TOP-REAL (n + 1))),1))
by A61, XBOOLE_0:def 4;
then consider w being
Real such that A62:
w > 0
and A63:
Ball (
Q,
w)
c= W /\ (Ball ((0. (TOP-REAL (n + 1))),1))
by A60, GOBOARD6:5;
set B =
Ball (
q,
w);
A64:
Ball (
Q,
w)
= Ball (
q,
w)
by TOPREAL9:13;
consider u being
object such that A65:
u in dom h
and A66:
u in FIU
and A67:
h . u = q
by FUNCT_1:def 6, A58;
reconsider u =
u as
Point of
M by A66;
A68:
Ball (
(0. (TOP-REAL (n + 1))),1)
c= cl_Ball (
(0. (TOP-REAL (n + 1))),1)
by A55, XBOOLE_1:11;
W /\ (Ball ((0. (TOP-REAL (n + 1))),1)) c= Ball (
(0. (TOP-REAL (n + 1))),1)
by XBOOLE_1:17;
then A69:
Ball (
q,
w)
c= Ball (
(0. (TOP-REAL (n + 1))),1)
by A63, A64;
then reconsider BB =
Ball (
q,
w) as
Subset of
(Tdisk ((0. (TOP-REAL (n + 1))),1)) by A68, XBOOLE_1:1, A38;
reconsider hBB =
h " BB as
Subset of
M by A12, XBOOLE_1:1;
A70:
Ball (
q,
w)
in the
topology of
(TOP-REAL (n + 1))
by PRE_TOPC:def 2;
|.(q - q).| = 0
by TOPRNS_1:28;
then
q in BB
by A62;
then A71:
u in hBB
by A65, A67, FUNCT_1:def 7;
A72:
(TOP-REAL (n + 1)) | (Ball (q,w)) = Tball (
q,
w)
by MFOLD_1:def 2;
BB /\ (cl_Ball ((0. (TOP-REAL (n + 1))),1)) = BB
by A68, XBOOLE_1:1, A69, XBOOLE_1:28;
then
BB in the
topology of
(Tdisk ((0. (TOP-REAL (n + 1))),1))
by A70, A38, PRE_TOPC:def 4;
then
BB is
open
by PRE_TOPC:def 2;
then A73:
h " BB is
open
by TOPGRP_1:26, A9, A6;
W /\ (Ball ((0. (TOP-REAL (n + 1))),1)) c= W
by XBOOLE_1:17;
then
BB c= W
by A63, A64;
then
BB c= h .: IU
by XBOOLE_1:19, A14;
then
h " BB c= Int U
by RELAT_1:143, A44;
then
hBB is
open
by A10, A12, A73, TSEP_1:9;
then A74:
Int hBB = hBB
by TOPS_1:23;
A75:
(Tdisk ((0. (TOP-REAL (n + 1))),1)) | BB = (TOP-REAL (n + 1)) | (Ball (q,w))
by A38, PRE_TOPC:7;
reconsider hBB =
hBB as
a_neighborhood of
u by A74, A71, CONNSP_2:def 1;
A76:
h .: hBB = BB
by FUNCT_1:77, A53;
A77:
(M | U) | (h " BB) = M | hBB
by A12, PRE_TOPC:7;
then reconsider hB =
h | hBB as
Function of
(M | hBB),
((TOP-REAL (n + 1)) | (Ball (q,w))) by JORDAN24:12, A75, A76;
hB is
being_homeomorphism
by A9, A6, A75, A76, A77, METRIZTS:2;
then A78:
M | hBB,
Tball (
q,
w)
are_homeomorphic
by A72, T_0TOPSP:def 1;
Tball (
q,
w),
Tball (
(0. (TOP-REAL (n + 1))),1)
are_homeomorphic
by A62, MFOLD_1:9;
then
M | hBB,
Tball (
(0. (TOP-REAL (n + 1))),1)
are_homeomorphic
by A78, A62, BORSUK_3:3;
then A79:
u in Int M
by Def3;
u in Fr M
by A66, XBOOLE_0:def 4;
then
u in ([#] M) \ (Int M)
by SUBSET_1:def 4;
hence
contradiction
by XBOOLE_0:def 5, A79;
verum
end;
x in Ball (
hp,
(min ((s / 2),(1 / 2))))
by A57, XBOOLE_0:def 4;
hence
x in (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2)))))
by A59, XBOOLE_0:def 4;
verum
end;
((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2)))))) /\ (Ball (hp,(min ((s / 2),(1 / 2))))) =
(Sphere ((0. (TOP-REAL (n + 1))),1)) /\ ((Ball (hp,(min ((s / 2),(1 / 2))))) /\ (Ball (hp,(min ((s / 2),(1 / 2))))))
by XBOOLE_1:16
.=
(Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2)))))
;
then A80:
hFIU /\ (Ball (hp,(min ((s / 2),(1 / 2))))) = (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2)))))
by A56, XBOOLE_1:26, BB;
reconsider v0 = (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2))))) as Subset of ((TOP-REAL (n + 1)) | hFIU) by A39, BB;
Ball (hp,(min ((s / 2),(1 / 2)))) in the topology of (TOP-REAL (n + 1))
by PRE_TOPC:def 2;
then
v0 in the topology of ((TOP-REAL (n + 1)) | hFIU)
by A80, PRE_TOPC:def 4, A39;
then A81:
v0 is open
by PRE_TOPC:def 2;
A82:
(Ball ((0. (TOP-REAL n)),1)) \/ (Sphere ((0. (TOP-REAL n)),1)) = cl_Ball ((0. (TOP-REAL n)),1)
by TOPREAL9:18;
A83:
Tball ((0. (TOP-REAL n)),1) = (TOP-REAL n) | (Ball ((0. (TOP-REAL n)),1))
by MFOLD_1:def 2;
A84:
|.(hp - (0. (TOP-REAL (n + 1)))).| = |.((0. (TOP-REAL (n + 1))) - hp).|
by TOPRNS_1:27;
A85:
min ((s / 2),(1 / 2)) > 0
by A20, XXREAL_0:21;
then A86:
|.((0. (TOP-REAL (n + 1))) - hp).| < 1 + (min ((s / 2),(1 / 2)))
by A19, A84, XREAL_1:29;
|.(hp - hp).| = 0
by TOPRNS_1:28;
then
hp in Ball (hp,(min ((s / 2),(1 / 2))))
by A85;
then A87:
hp in (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2)))))
by A9, A7, XBOOLE_0:def 4;
A88:
pF in Int U
by A4, CONNSP_2:def 1;
then A89:
pF in h " ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2))))))
by A16, A10, A12, A4, A87, FUNCT_1:def 7;
min ((s / 2),(1 / 2)) <= 1 / 2
by XXREAL_0:17;
then
min ((s / 2),(1 / 2)) < |.((0. (TOP-REAL (n + 1))) - hp).|
by A19, A84, XXREAL_0:2;
then consider g being Function of ((TOP-REAL (n + 1)) | ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (hp,(min ((s / 2),(1 / 2))))))),(Tdisk ((0. (TOP-REAL n)),1)) such that
A90:
g is being_homeomorphism
and
A91:
g .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (hp,(min ((s / 2),(1 / 2)))))) = Sphere ((0. (TOP-REAL n)),1)
by A19, A84, A86, BROUWER3:19;
A92:
(g .: (Sphere ((0. (TOP-REAL (n + 1))),1))) /\ (g .: (Ball (hp,(min ((s / 2),(1 / 2)))))) = g .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2))))))
by A90, FUNCT_1:62;
A93:
[#] ((M | U) | FIU) = FIU
by PRE_TOPC:def 5;
then reconsider U0 = h " ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2)))))) as non empty Subset of ((M | U) | FIU) by A52, A25, XBOOLE_1:19, A16, A88, A4, A87, FUNCT_1:def 7;
reconsider U0 = h " ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2)))))) as Subset of ((M | U) | FIU) by A52, A25, XBOOLE_1:19, A93;
A94:
[#] ((M | (Fr M)) | FIU1) = FIU
by PRE_TOPC:def 5;
then reconsider u0 = U0 as Subset of ((M | (Fr M)) | FIU1) by A93;
hfiu " v0 = FIU /\ U0
by FUNCT_1:70;
then
hfiu " v0 = U0
by A52, A25, XBOOLE_1:19, XBOOLE_1:28;
then A95:
U0 is open
by A81, A41, TOPGRP_1:26;
reconsider FV0 = u0 as Subset of (M | (Fr M)) by XBOOLE_1:1, A93;
A96:
(Fr M) /\ (Int U) c= (Fr M) /\ U
by XBOOLE_1:26, TOPS_1:16;
then
(M | U) | FIU = M | ((Fr M) /\ (Int U))
by A36, XBOOLE_1:1, PRE_TOPC:7;
then
FV0 is open
by A34, A35, A95, TSEP_1:9, A94;
then
pF in Int FV0
by A89, TOPS_1:22;
then reconsider FV0 = FV0 as a_neighborhood of pF by CONNSP_2:def 1;
reconsider MV0 = FV0 as Subset of M by A52, XBOOLE_1:1;
h " ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2)))))) c= IU /\ (Fr M)
by A52, A25, XBOOLE_1:19;
then
FV0 c= (Fr M) /\ U
by A96;
then A97:
(M | U) | (h " ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2))))))) = M | MV0
by PRE_TOPC:7, A36, XBOOLE_1:1;
(Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (hp,(min ((s / 2),(1 / 2))))) misses (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2)))))
by TOPREAL9:19, XBOOLE_1:76;
then A98:
Sphere ((0. (TOP-REAL n)),1) misses g .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2))))))
by A90, A91, FUNCT_1:66;
A99:
(g .: (Sphere ((0. (TOP-REAL (n + 1))),1))) /\ (g .: (Sphere (hp,(min ((s / 2),(1 / 2)))))) = g .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (hp,(min ((s / 2),(1 / 2))))))
by A90, FUNCT_1:62;
A100:
[#] ((TOP-REAL (n + 1)) | ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (hp,(min ((s / 2),(1 / 2))))))) = (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (hp,(min ((s / 2),(1 / 2)))))
by PRE_TOPC:def 5;
then A101:
dom g = (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (hp,(min ((s / 2),(1 / 2)))))
by A90, TOPS_2:def 5;
A102:
(Ball (hp,(min ((s / 2),(1 / 2))))) \/ (Sphere (hp,(min ((s / 2),(1 / 2))))) = cl_Ball (hp,(min ((s / 2),(1 / 2))))
by TOPREAL9:18;
then reconsider ZV0 = (Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2))))) as Subset of ((TOP-REAL (n + 1)) | ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (hp,(min ((s / 2),(1 / 2))))))) by XBOOLE_1:7, XBOOLE_1:26, A100;
A103:
g .: (cl_Ball (hp,(min ((s / 2),(1 / 2))))) = (g .: (Ball (hp,(min ((s / 2),(1 / 2)))))) \/ (g .: (Sphere (hp,(min ((s / 2),(1 / 2))))))
by A102, RELAT_1:120;
A104:
[#] (Tdisk ((0. (TOP-REAL n)),1)) = cl_Ball ((0. (TOP-REAL n)),1)
by PRE_TOPC:def 5;
then
rng g = cl_Ball ((0. (TOP-REAL n)),1)
by A90, TOPS_2:def 5;
then cl_Ball ((0. (TOP-REAL n)),1) =
g .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (hp,(min ((s / 2),(1 / 2))))))
by A101, RELAT_1:113
.=
(g .: (Sphere ((0. (TOP-REAL (n + 1))),1))) /\ (g .: (cl_Ball (hp,(min ((s / 2),(1 / 2))))))
by A90, FUNCT_1:62
.=
(g .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2))))))) \/ (Sphere ((0. (TOP-REAL n)),1))
by A103, A99, A92, A91, XBOOLE_1:23
;
then
g .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2)))))) = Ball ((0. (TOP-REAL n)),1)
by A82, A42, A98, XBOOLE_1:71;
then A105:
(Tdisk ((0. (TOP-REAL n)),1)) | (g .: ZV0) = Tball ((0. (TOP-REAL n)),1)
by PRE_TOPC:7, A83, A104;
A106:
((TOP-REAL (n + 1)) | ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (hp,(min ((s / 2),(1 / 2))))))) | ZV0 = (TOP-REAL (n + 1)) | ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2))))))
by A100, PRE_TOPC:7;
then reconsider GG = g | ZV0 as Function of ((TOP-REAL (n + 1)) | ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2))))))),(Tball ((0. (TOP-REAL n)),1)) by A87, JORDAN24:12, A105;
A107:
GG is being_homeomorphism
by A90, METRIZTS:2, A106, A105;
A108:
M | MV0 = (M | (Fr M)) | FV0
by A5, PRE_TOPC:7;
then reconsider HH = h | FV0 as Function of ((M | (Fr M)) | FV0),((TOP-REAL (n + 1)) | ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Ball (hp,(min ((s / 2),(1 / 2))))))) by A97, A54, JORDAN24:12;
reconsider GH = GG * HH as Function of ((M | (Fr M)) | FV0),(Tball ((0. (TOP-REAL n)),1)) by A87;
take
FV0
; (M | (Fr M)) | FV0, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
HH is being_homeomorphism
by A9, A6, METRIZTS:2, A97, A54, A108;
then
GH is being_homeomorphism
by A87, A107, TOPS_2:57;
hence
(M | (Fr M)) | FV0, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
by T_0TOPSP:def 1; verum