let M be non empty locally_euclidean TopSpace; for p being Point of M holds
( p in Fr M iff ex U being a_neighborhood of p ex n being Nat ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) )
let p be Point of M; ( p in Fr M iff ex U being a_neighborhood of p ex n being Nat ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) )
thus
( p in Fr M implies ex U being a_neighborhood of p ex n being Nat ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) )
( ex U being a_neighborhood of p ex n being Nat ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) ) implies p in Fr M )proof
assume A1:
p in Fr M
;
ex U being a_neighborhood of p ex n being Nat ex h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism & h . p in Sphere ((0. (TOP-REAL n)),1) )
consider U being
a_neighborhood of
p,
n being
Nat such that A2:
M | U,
Tdisk (
(0. (TOP-REAL n)),1)
are_homeomorphic
by Def2;
set TR =
TOP-REAL n;
consider h being
Function of
(M | U),
(Tdisk ((0. (TOP-REAL n)),1)) such that A3:
h is
being_homeomorphism
by A2, T_0TOPSP:def 1;
assume
for
U being
a_neighborhood of
p for
n being
Nat for
h being
Function of
(M | U),
(Tdisk ((0. (TOP-REAL n)),1)) st
h is
being_homeomorphism holds
not
h . p in Sphere (
(0. (TOP-REAL n)),1)
;
contradiction
then A4:
not
h . p in Sphere (
(0. (TOP-REAL n)),1)
by A3;
A5:
Ball (
(0. (TOP-REAL n)),1)
in the
topology of
(TOP-REAL n)
by PRE_TOPC:def 2;
A6:
p in Int U
by CONNSP_2:def 1;
A7:
Int U in the
topology of
M
by PRE_TOPC:def 2;
A8:
[#] (M | U) = U
by PRE_TOPC:def 5;
then reconsider IU =
Int U as
Subset of
(M | U) by TOPS_1:16;
IU /\ U = IU
by TOPS_1:16, XBOOLE_1:28;
then
IU in the
topology of
(M | U)
by A7, A8, PRE_TOPC:def 4;
then reconsider IU =
IU as non
empty open Subset of
(M | U) by CONNSP_2:def 1, PRE_TOPC:def 2;
A9:
[#] ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) = cl_Ball (
(0. (TOP-REAL n)),1)
by PRE_TOPC:def 5;
then reconsider hIU =
h .: IU as
Subset of
(TOP-REAL n) by XBOOLE_1:1;
A10:
h .: IU is
open
by A3, TOPGRP_1:25;
A11:
dom h = [#] (M | U)
by A3, TOPS_2:def 5;
then A12:
h " (h .: IU) = IU
by FUNCT_1:94, A3;
A13:
cl_Ball (
(0. (TOP-REAL n)),1)
= (Ball ((0. (TOP-REAL n)),1)) \/ (Sphere ((0. (TOP-REAL n)),1))
by TOPREAL9:18;
then reconsider B =
Ball (
(0. (TOP-REAL n)),1) as
Subset of
((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) by A9, XBOOLE_1:7;
(Ball ((0. (TOP-REAL n)),1)) /\ (cl_Ball ((0. (TOP-REAL n)),1)) = Ball (
(0. (TOP-REAL n)),1)
by A13, XBOOLE_1:7, XBOOLE_1:28;
then
B in the
topology of
((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1)))
by A5, A9, PRE_TOPC:def 4;
then reconsider B =
B as non
empty open Subset of
((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) by PRE_TOPC:def 2;
reconsider BhIU =
B /\ (h .: IU) as
Subset of
(TOP-REAL n) by XBOOLE_1:1, A9;
BhIU c= Ball (
(0. (TOP-REAL n)),1)
by XBOOLE_1:17;
then A14:
BhIU is
open
by A10, TSEP_1:9;
A15:
Int U c= U
by TOPS_1:16;
then
h . p in rng h
by A6, A8, A11, FUNCT_1:def 3;
then A16:
h . p in Ball (
(0. (TOP-REAL n)),1)
by A4, A9, A13, XBOOLE_0:def 3;
then reconsider hp =
h . p as
Point of
(TOP-REAL n) ;
TopStruct(# the
carrier of
(TOP-REAL n), the
topology of
(TOP-REAL n) #)
= TopSpaceMetr (Euclid n)
by EUCLID:def 8;
then reconsider HP =
hp as
Point of
(Euclid n) by TOPMETR:12;
h . p in h .: IU
by A11, A6, FUNCT_1:def 6;
then
h . p in BhIU
by A16, XBOOLE_0:def 4;
then
hp in Int BhIU
by A14, TOPS_1:23;
then consider s being
Real such that A17:
s > 0
and A18:
Ball (
HP,
s)
c= BhIU
by GOBOARD6:5;
set W =
Ball (
hp,
s);
reconsider hW =
h " (Ball (hp,s)) as
Subset of
M by A8, XBOOLE_1:1;
A19:
Ball (
hp,
s)
c= B /\ (h .: IU)
by A18, TOPREAL9:13;
then reconsider w =
Ball (
hp,
s) as
Subset of
((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) by XBOOLE_1:1;
A20:
w in the
topology of
(TOP-REAL n)
by PRE_TOPC:def 2;
hp is
Element of
REAL n
by EUCLID:22;
then
|.(hp - hp).| = 0
;
then
hp in Ball (
hp,
s)
by A17;
then A21:
p in hW
by A8, A11, A15, A6, FUNCT_1:def 7;
rng h = [#] ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1)))
by A3, TOPS_2:def 5;
then
h .: (h " (Ball (hp,s))) = Ball (
hp,
s)
by A19, XBOOLE_1:1, FUNCT_1:77;
then A22:
(Tdisk ((0. (TOP-REAL n)),1)) | (h .: (h " (Ball (hp,s)))) = (TOP-REAL n) | (Ball (hp,s))
by A9, PRE_TOPC:7;
w /\ (cl_Ball ((0. (TOP-REAL n)),1)) = w
by A9, XBOOLE_1:28;
then A23:
w in the
topology of
((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1)))
by A9, A20, PRE_TOPC:def 4;
B /\ (h .: IU) c= h .: IU
by XBOOLE_1:17;
then
Ball (
hp,
s)
c= h .: IU
by A19;
then A24:
hW c= IU
by A12, RELAT_1:143;
reconsider w =
w as
open Subset of
((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) by A23, PRE_TOPC:def 2;
reconsider hh =
h | (h " w) as
Function of
((M | U) | (h " w)),
((Tdisk ((0. (TOP-REAL n)),1)) | (h .: (h " w))) by JORDAN24:12;
A25:
(M | U) | (h " (Ball (hp,s))) = M | hW
by A8, PRE_TOPC:7;
then reconsider HH =
hh as
Function of
(M | hW),
((TOP-REAL n) | (Ball (hp,s))) by A22;
h " w is
open
by A3, TOPGRP_1:26;
then
hW is
open
by A24, TSEP_1:9;
then
p in Int hW
by A21, TOPS_1:23;
then reconsider HW =
hW as
a_neighborhood of
p by CONNSP_2:def 1;
HH is
being_homeomorphism
by A3, METRIZTS:2, A22, A25;
then A27:
M | HW,
(TOP-REAL n) | (Ball (hp,s)) are_homeomorphic
by T_0TOPSP:def 1;
Tball (
hp,
s),
Tball (
(0. (TOP-REAL n)),1)
are_homeomorphic
by A17, Th3;
then
M | HW,
Tball (
(0. (TOP-REAL n)),1)
are_homeomorphic
by A27, A17, BORSUK_3:3;
then
p in Int M
by Def4;
then
not
p in ([#] M) \ (Int M)
by XBOOLE_0:def 5;
hence
contradiction
by SUBSET_1:def 4, A1;
verum
end;
given U being a_neighborhood of p, n being Nat, h being Function of (M | U),(Tdisk ((0. (TOP-REAL n)),1)) such that A28:
h is being_homeomorphism
and
A29:
h . p in Sphere ((0. (TOP-REAL n)),1)
; p in Fr M
set TR = TOP-REAL n;
A30:
p in Int U
by CONNSP_2:def 1;
assume
not p in Fr M
; contradiction
then
not p in ([#] M) \ (Int M)
by SUBSET_1:def 4;
then
p in Int M
by XBOOLE_0:def 5;
then consider W being a_neighborhood of p, m being Nat such that
A31:
M | W, Tball ((0. (TOP-REAL m)),1) are_homeomorphic
by Def4;
A33:
p in Int W
by CONNSP_2:def 1;
M | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic
by A28, T_0TOPSP:def 1;
then
m = n
by A30, A33, XBOOLE_0:3, BROUWER3:15, A31;
then consider g being Function of (M | W),((TOP-REAL n) | (Ball ((0. (TOP-REAL n)),1))) such that
A34:
g is being_homeomorphism
by A31, T_0TOPSP:def 1;
A35:
Int U c= U
by TOPS_1:16;
set I = (Int U) /\ (Int W);
A36:
[#] (M | U) = U
by PRE_TOPC:def 5;
(Int U) /\ (Int W) c= Int U
by XBOOLE_1:17;
then reconsider IU = (Int U) /\ (Int W) as non empty open Subset of (M | U) by XBOOLE_1:1, A35, A36, A30, A33, XBOOLE_0:def 4, TSEP_1:9;
A37:
dom h = [#] (M | U)
by A28, TOPS_2:def 5;
then A38:
h " (h .: IU) = IU
by A28, FUNCT_1:94;
p in (Int U) /\ (Int W)
by A30, A33, XBOOLE_0:def 4;
then A39:
h . p in h .: IU
by A37, FUNCT_1:def 6;
h .: IU is open
by A28, TOPGRP_1:25;
then
h .: IU in the topology of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1)))
by PRE_TOPC:def 2;
then consider Q being Subset of (TOP-REAL n) such that
A40:
Q in the topology of (TOP-REAL n)
and
A41:
h .: IU = Q /\ ([#] ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))))
by PRE_TOPC:def 4;
reconsider Q = Q as non empty Subset of (TOP-REAL n) by A41;
A42:
Int Q = Q
by A40, PRE_TOPC:def 2, TOPS_1:23;
A43:
(Int U) /\ (Int W) c= Int W
by XBOOLE_1:17;
A44:
[#] ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) = cl_Ball ((0. (TOP-REAL n)),1)
by PRE_TOPC:def 5;
then
h . p in cl_Ball ((0. (TOP-REAL n)),1)
by A39;
then reconsider hp = h . p as Point of (TOP-REAL n) ;
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n)
by EUCLID:def 8;
then reconsider HP = hp as Point of (Euclid n) by TOPMETR:12;
hp in Q
by A39, A41, XBOOLE_0:def 4;
then consider s being Real such that
A45:
s > 0
and
A46:
Ball (HP,s) c= Q
by A42, GOBOARD6:5;
set s2 = s / 2;
hp is Element of REAL n
by EUCLID:22;
then
|.(hp - hp).| = 0
;
then A47:
hp in Ball (hp,(s / 2))
by A45;
set clb = (cl_Ball (hp,(s / 2))) /\ (cl_Ball ((0. (TOP-REAL n)),1));
A48:
Ball (hp,(s / 2)) c= cl_Ball (hp,(s / 2))
by TOPREAL9:16;
(cl_Ball (hp,(s / 2))) /\ (cl_Ball ((0. (TOP-REAL n)),1)) = (cl_Ball (hp,(s / 2))) /\ ([#] ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))))
by PRE_TOPC:def 5;
then reconsider CLB = (cl_Ball (hp,(s / 2))) /\ (cl_Ball ((0. (TOP-REAL n)),1)) as non empty Subset of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) by A48, A47, A39, XBOOLE_0:def 4;
A49:
rng h = [#] ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1)))
by A28, TOPS_2:def 5;
then reconsider hCLB = h " CLB as non empty Subset of (M | U) by RELAT_1:139;
A50:
Ball (HP,s) = Ball (hp,s)
by TOPREAL9:13;
hp in CLB
by A48, A47, A39, A44, XBOOLE_0:def 4;
then A51:
p in hCLB
by A37, A36, A35, A30, FUNCT_1:def 7;
n in NAT
by ORDINAL1:def 12;
then A52:
cl_Ball (hp,(s / 2)) c= Ball (hp,s)
by XREAL_1:216, A45, JORDAN:21;
then
cl_Ball (hp,(s / 2)) c= Q
by A46, A50;
then
CLB c= h .: IU
by A44, XBOOLE_1:26, A41;
then A53:
hCLB c= IU
by RELAT_1:143, A38;
reconsider BB = (Ball (hp,(s / 2))) /\ ([#] ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1)))) as Subset of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) ;
reconsider hBB = h " BB as Subset of M by A36, XBOOLE_1:1;
Ball (hp,(s / 2)) c= Q
by A46, A50, A48, A52;
then
BB c= h .: IU
by XBOOLE_1:26, A41;
then A54:
h " BB c= IU
by RELAT_1:143, A38;
reconsider HCLB = hCLB as non empty Subset of M by A36, XBOOLE_1:1;
A55:
h .: hCLB = CLB
by A49, FUNCT_1:77;
A56:
((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1))) | CLB = (TOP-REAL n) | ((cl_Ball (hp,(s / 2))) /\ (cl_Ball ((0. (TOP-REAL n)),1)))
by A44, PRE_TOPC:7;
A57:
(M | U) | hCLB = M | HCLB
by A36, PRE_TOPC:7;
then reconsider h1 = h | hCLB as Function of (M | HCLB),((TOP-REAL n) | ((cl_Ball (hp,(s / 2))) /\ (cl_Ball ((0. (TOP-REAL n)),1)))) by A56, A55, JORDAN24:12;
A58:
Int W c= W
by TOPS_1:16;
A59:
[#] (M | W) = W
by PRE_TOPC:def 5;
then reconsider IW = (Int U) /\ (Int W) as non empty open Subset of (M | W) by A30, A33, XBOOLE_0:def 4, XBOOLE_1:1, A58, A43, TSEP_1:9;
A60:
IU c= W
by A58, A43;
then reconsider hCLW = hCLB as non empty Subset of (M | W) by A53, XBOOLE_1:1, A59;
A61:
(M | W) | hCLW = M | HCLB
by A53, A60, XBOOLE_1:1, PRE_TOPC:7;
set ghCLW = g .: hCLW;
A62:
[#] ((TOP-REAL n) | (Ball ((0. (TOP-REAL n)),1))) = Ball ((0. (TOP-REAL n)),1)
by PRE_TOPC:def 5;
then reconsider GhCLW = g .: hCLW as non empty Subset of (TOP-REAL n) by XBOOLE_1:1;
A63:
((TOP-REAL n) | (Ball ((0. (TOP-REAL n)),1))) | (g .: hCLW) = (TOP-REAL n) | GhCLW
by A62, PRE_TOPC:7;
then reconsider g1 = g | hCLB as Function of (M | HCLB),((TOP-REAL n) | GhCLW) by A61, JORDAN24:12;
A64:
g1 is being_homeomorphism
by A34, METRIZTS:2, A63, A61;
then A65:
g1 " is being_homeomorphism
by TOPS_2:56;
A66:
dom g = [#] (M | W)
by A34, TOPS_2:def 5;
then
g . p in GhCLW
by A51, FUNCT_1:def 6;
then reconsider gp = g . p as Point of (TOP-REAL n) ;
(Int U) /\ (Int W) c= W
by A58, A43;
then reconsider hBW = hBB as Subset of (M | W) by A54, XBOOLE_1:1, A59;
reconsider ghBW = g .: hBW as Subset of (TOP-REAL n) by A62, XBOOLE_1:1;
hp in BB
by A47, A39, XBOOLE_0:def 4;
then
p in h " BB
by A37, A36, A35, A30, FUNCT_1:def 7;
then A67:
gp in ghBW
by A66, FUNCT_1:def 6;
set hg = h1 * (g1 ");
h1 is being_homeomorphism
by A28, A56, METRIZTS:2, A57, A55;
then A68:
h1 * (g1 ") is being_homeomorphism
by A65, TOPS_2:57;
then A69:
dom (h1 * (g1 ")) = [#] ((TOP-REAL n) | GhCLW)
by TOPS_2:def 5;
BB c= (cl_Ball (hp,(s / 2))) /\ (cl_Ball ((0. (TOP-REAL n)),1))
by TOPREAL9:16, XBOOLE_1:26, A44;
then A70:
hBB c= hCLB
by RELAT_1:143;
then
ghBW c= GhCLW
by RELAT_1:123;
then
gp in GhCLW
by A67;
then A71:
gp in dom (h1 * (g1 "))
by A69, PRE_TOPC:def 5;
Ball (hp,(s / 2)) in the topology of (TOP-REAL n)
by PRE_TOPC:def 2;
then
BB in the topology of ((TOP-REAL n) | (cl_Ball ((0. (TOP-REAL n)),1)))
by PRE_TOPC:def 4;
then
( not BB is empty & BB is open )
by A47, A39, XBOOLE_0:def 4, PRE_TOPC:def 2;
then
h " BB is open
by A28, TOPGRP_1:26;
then
hBB is open
by A54, TSEP_1:9;
then
hBW is open
by TSEP_1:9;
then
g .: hBW is open
by A34, TOPGRP_1:25;
then
ghBW is open
by A62, TSEP_1:9;
then
gp in Int GhCLW
by A67, TOPS_1:22, A70, RELAT_1:123;
then A72:
(h1 * (g1 ")) . gp in Int ((cl_Ball (hp,(s / 2))) /\ (cl_Ball ((0. (TOP-REAL n)),1)))
by BROUWER3:11, A68;
Int ((cl_Ball (hp,(s / 2))) /\ (cl_Ball ((0. (TOP-REAL n)),1))) = (Int (cl_Ball (hp,(s / 2)))) /\ (Int (cl_Ball ((0. (TOP-REAL n)),1)))
by TOPS_1:17;
then A73:
(h1 * (g1 ")) . gp in Int (cl_Ball ((0. (TOP-REAL n)),1))
by A72, XBOOLE_0:def 4;
reconsider G1 = g1 as Function ;
Fr (cl_Ball ((0. (TOP-REAL n)),1)) = Sphere ((0. (TOP-REAL n)),1)
by BROUWER2:5;
then A74:
Int (cl_Ball ((0. (TOP-REAL n)),1)) = (cl_Ball ((0. (TOP-REAL n)),1)) \ (Sphere ((0. (TOP-REAL n)),1))
by TOPS_1:40;
A75:
G1 " = g1 "
by A64, TOPS_2:def 4;
dom g1 = [#] (M | HCLB)
by A64, TOPS_2:def 5;
then
p in dom g1
by PRE_TOPC:def 5, A51;
then A76:
(g1 ") . (g1 . p) = p
by A64, A75, FUNCT_1:34;
A77:
g . p = g1 . p
by A51, FUNCT_1:49;
then A78:
p in dom h1
by A71, FUNCT_1:11, A76;
(h1 * (g1 ")) . gp = h1 . p
by A71, FUNCT_1:12, A76, A77;
then
(h1 * (g1 ")) . gp = h . p
by A78, FUNCT_1:47;
hence
contradiction
by A29, A73, A74, XBOOLE_0:def 5; verum