A1:
for x being set holds
( x in Int M iff ex U being Subset of M st
( U is open & U c= Int M & x in U ) )
set p = the Point of M;
consider U being a_neighborhood of the Point of M, n being Nat such that
A5:
M | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic
by Def2;
A6:
[#] (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;
set TR = TOP-REAL n;
consider h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) such that
A7:
h is being_homeomorphism
by T_0TOPSP:def 1, A5;
IU is open
by TSEP_1:9;
then
h .: IU is open
by A7, TOPGRP_1:25;
then
h .: IU in the topology of (Tdisk ((0. (TOP-REAL n)),1))
by PRE_TOPC:def 2;
then consider W being Subset of (TOP-REAL n) such that
A8:
W in the topology of (TOP-REAL n)
and
A9:
h .: IU = W /\ ([#] (Tdisk ((0. (TOP-REAL n)),1)))
by PRE_TOPC:def 4;
A10:
[#] (Tdisk ((0. (TOP-REAL n)),1)) = cl_Ball ((0. (TOP-REAL n)),1)
by PRE_TOPC:def 5;
A11:
dom h = [#] (M | U)
by A7, TOPS_2:def 5;
A12:
Ball ((0. (TOP-REAL n)),1) c= cl_Ball ((0. (TOP-REAL n)),1)
by TOPREAL9:16;
reconsider W = W as open Subset of (TOP-REAL n) by A8, PRE_TOPC:def 2;
set WB = W /\ (Ball ((0. (TOP-REAL n)),1));
the Point of M in Int U
by CONNSP_2:def 1;
then A13:
h . the Point of M in h .: IU
by A11, FUNCT_1:def 6;
then A14:
h . the Point of M in W
by A9, XBOOLE_0:def 4;
then reconsider hp = h . the Point of M as Point of (TOP-REAL n) ;
A15:
h .: IU = W /\ (cl_Ball ((0. (TOP-REAL n)),1))
by PRE_TOPC:def 5, A9;
not W /\ (Ball ((0. (TOP-REAL n)),1)) is empty
proof
reconsider HP =
hp as
Point of
(Euclid n) by EUCLID:67;
A16:
Ball (
(0. (TOP-REAL n)),1)
misses Sphere (
(0. (TOP-REAL n)),1)
by TOPREAL9:19;
A17:
cl_Ball (
(0. (TOP-REAL n)),1)
= (Ball ((0. (TOP-REAL n)),1)) \/ (Sphere ((0. (TOP-REAL n)),1))
by TOPREAL9:18;
assume A18:
W /\ (Ball ((0. (TOP-REAL n)),1)) is
empty
;
contradiction
then W /\ (cl_Ball ((0. (TOP-REAL n)),1)) =
(W /\ (cl_Ball ((0. (TOP-REAL n)),1))) \ (W /\ (Ball ((0. (TOP-REAL n)),1)))
.=
((W /\ (cl_Ball ((0. (TOP-REAL n)),1))) \ W) \/ ((W /\ (cl_Ball ((0. (TOP-REAL n)),1))) \ (Ball ((0. (TOP-REAL n)),1)))
by XBOOLE_1:54
.=
{} \/ ((W /\ (cl_Ball ((0. (TOP-REAL n)),1))) \ (Ball ((0. (TOP-REAL n)),1)))
by XBOOLE_1:17, XBOOLE_1:37
.=
W /\ ((cl_Ball ((0. (TOP-REAL n)),1)) \ (Ball ((0. (TOP-REAL n)),1)))
by XBOOLE_1:49
.=
W /\ (Sphere ((0. (TOP-REAL n)),1))
by A16, A17, XBOOLE_1:88
;
then
hp in Sphere (
(0. (TOP-REAL n)),1)
by A15, A13, XBOOLE_0:def 4;
then A19:
|.hp.| = 1
by TOPREAL9:12;
Int W = W
by TOPS_1:23;
then consider s being
Real such that A20:
s > 0
and A21:
Ball (
HP,
s)
c= W
by A14, GOBOARD6:5;
set s2 =
s / 2;
set m =
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:
min (
(s / 2),
(1 / 2))
< s
by A22, XXREAL_0:2;
A24:
Ball (
HP,
s)
= Ball (
hp,
s)
by TOPREAL9:13;
A25:
min (
(s / 2),
(1 / 2))
> 0
by A20, XXREAL_0:21;
then A26:
1
- (min ((s / 2),(1 / 2))) < 1
- 0
by XREAL_1:6;
A27:
|.(- (min ((s / 2),(1 / 2)))).| = - (- (min ((s / 2),(1 / 2))))
by A25, ABSVALUE:def 1;
A28:
((1 - (min ((s / 2),(1 / 2)))) * hp) - (0. (TOP-REAL n)) = (1 - (min ((s / 2),(1 / 2)))) * hp
by RLVECT_1:13;
((1 - (min ((s / 2),(1 / 2)))) * hp) - hp =
((1 - (min ((s / 2),(1 / 2)))) * hp) - (1 * hp)
by RLVECT_1:def 8
.=
((1 - (min ((s / 2),(1 / 2)))) - 1) * hp
by RLVECT_1:35
.=
(- (min ((s / 2),(1 / 2)))) * hp
;
then
|.(((1 - (min ((s / 2),(1 / 2)))) * hp) - hp).| = |.(- (min ((s / 2),(1 / 2)))).| * 1
by A19, EUCLID:11;
then A29:
(1 - (min ((s / 2),(1 / 2)))) * hp in Ball (
hp,
s)
by A27, A23;
1
- (min ((s / 2),(1 / 2))) >= 1
- (1 / 2)
by XXREAL_0:17, XREAL_1:10;
then
|.(1 - (min ((s / 2),(1 / 2)))).| = 1
- (min ((s / 2),(1 / 2)))
by ABSVALUE:def 1;
then
|.((1 - (min ((s / 2),(1 / 2)))) * hp).| = (1 - (min ((s / 2),(1 / 2)))) * 1
by A19, EUCLID:11;
then
(1 - (min ((s / 2),(1 / 2)))) * hp in Ball (
(0. (TOP-REAL n)),1)
by A28, A26;
hence
contradiction
by A29, A21, A24, A18, XBOOLE_0:def 4;
verum
end;
then consider wb being set such that
A30:
wb in W /\ (Ball ((0. (TOP-REAL n)),1))
;
reconsider wb = wb as Point of (TOP-REAL n) by A30;
reconsider wbE = wb as Point of (Euclid n) by EUCLID:67;
Int (W /\ (Ball ((0. (TOP-REAL n)),1))) = W /\ (Ball ((0. (TOP-REAL n)),1))
by TOPS_1:23;
then consider s being Real such that
A31:
s > 0
and
A32:
Ball (wbE,s) c= W /\ (Ball ((0. (TOP-REAL n)),1))
by A30, GOBOARD6:5;
A33:
Ball (wb,s) = Ball (wbE,s)
by TOPREAL9:13;
W /\ (Ball ((0. (TOP-REAL n)),1)) c= Ball ((0. (TOP-REAL n)),1)
by XBOOLE_1:17;
then A34:
Ball (wb,s) c= Ball ((0. (TOP-REAL n)),1)
by A32, A33;
then reconsider BB = Ball (wb,s) as Subset of (Tdisk ((0. (TOP-REAL n)),1)) by A12, XBOOLE_1:1, A10;
A35:
(Tdisk ((0. (TOP-REAL n)),1)) | BB = (TOP-REAL n) | (Ball (wb,s))
by A34, A12, XBOOLE_1:1, PRE_TOPC:7;
reconsider hBB = h " BB as Subset of M by A6, XBOOLE_1:1;
BB is open
by TSEP_1:9;
then A36:
h " BB is open
by A7, TOPGRP_1:26;
W /\ (Ball ((0. (TOP-REAL n)),1)) c= h .: IU
by A10, A9, TOPREAL9:16, XBOOLE_1:26;
then
BB c= h .: IU
by A32, A33;
then A37:
h " BB c= h " (h .: IU)
by RELAT_1:143;
h " (h .: IU) c= IU
by FUNCT_1:82, A7;
then
h " BB c= IU
by A37;
then
hBB is open
by A36, TSEP_1:9;
then A38:
Int hBB = hBB
by TOPS_1:23;
A39:
rng h = [#] (Tdisk ((0. (TOP-REAL n)),1))
by A7, TOPS_2:def 5;
then A40:
h .: (h " BB) = BB
by FUNCT_1:77;
not hBB is empty
by A31, RELAT_1:139, A39;
then consider t being set such that
A41:
t in hBB
;
reconsider t = t as Point of M by A41;
reconsider hBB = hBB as a_neighborhood of t by A38, CONNSP_2:def 1, A41;
A43:
(M | U) | (h " BB) = M | hBB
by A6, PRE_TOPC:7;
then reconsider HH = h | (h " BB) as Function of (M | hBB),((TOP-REAL n) | (Ball (wb,s))) by A40, A35, JORDAN24:12;
HH is being_homeomorphism
by A7, A40, A35, A43, METRIZTS:2;
then A44:
M | hBB,(TOP-REAL n) | (Ball (wb,s)) are_homeomorphic
by T_0TOPSP:def 1;
Tball (wb,s), Tball ((0. (TOP-REAL n)),1) are_homeomorphic
by Th3, A31;
then
M | hBB, Tball ((0. (TOP-REAL n)),1) are_homeomorphic
by A44, A31, BORSUK_3:3;
hence
( not Int M is empty & Int M is open )
by A1, TOPS_1:25, Def4; verum