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 Def1;
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;
A26:
(TOP-REAL n) | (Ball (hp,s)) = Tball (
hp,
s)
by MFOLD_1:def 2;
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, MFOLD_1:9;
then
M | HW,
Tball (
(0. (TOP-REAL n)),1)
are_homeomorphic
by A27, A26, A17, BORSUK_3:3;
then
p in Int M
by Def3;
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 Def3;
A:
Tball ((0. (TOP-REAL m)),1) = (TOP-REAL m) | (Ball ((0. (TOP-REAL m)),1))
by MFOLD_1:def 2;
A32:
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, A32, XBOOLE_0:3, A, BROUWER3:15, A31;
then
M | W,(TOP-REAL n) | (Ball ((0. (TOP-REAL n)),1)) are_homeomorphic
by A31, MFOLD_1:def 2;
then consider g being Function of (M | W),((TOP-REAL n) | (Ball ((0. (TOP-REAL n)),1))) such that
A33:
g is being_homeomorphism
by T_0TOPSP:def 1;
A34:
Int U c= U
by TOPS_1:16;
set I = (Int U) /\ (Int W);
A35:
[#] (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, A34, A35, A30, A32, XBOOLE_0:def 4, TSEP_1:9;
A36:
dom h = [#] (M | U)
by A28, TOPS_2:def 5;
then A37:
h " (h .: IU) = IU
by A28, FUNCT_1:94;
p in (Int U) /\ (Int W)
by A30, A32, XBOOLE_0:def 4;
then A38:
h . p in h .: IU
by A36, 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
A39:
Q in the topology of (TOP-REAL n)
and
A40:
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 A40;
A41:
Int Q = Q
by A39, PRE_TOPC:def 2, TOPS_1:23;
A42:
(Int U) /\ (Int W) c= Int W
by XBOOLE_1:17;
A43:
[#] ((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 A38;
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 A38, A40, XBOOLE_0:def 4;
then consider s being Real such that
A44:
s > 0
and
A45:
Ball (HP,s) c= Q
by A41, GOBOARD6:5;
set s2 = s / 2;
hp is Element of REAL n
by EUCLID:22;
then
|.(hp - hp).| = 0
;
then A46:
hp in Ball (hp,(s / 2))
by A44;
set clb = (cl_Ball (hp,(s / 2))) /\ (cl_Ball ((0. (TOP-REAL n)),1));
A47:
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 A47, A46, A38, XBOOLE_0:def 4;
A48:
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;
A49:
Ball (HP,s) = Ball (hp,s)
by TOPREAL9:13;
hp in CLB
by A47, A46, A38, A43, XBOOLE_0:def 4;
then A50:
p in hCLB
by A36, A35, A34, A30, FUNCT_1:def 7;
n in NAT
by ORDINAL1:def 12;
then A51:
cl_Ball (hp,(s / 2)) c= Ball (hp,s)
by XREAL_1:216, A44, JORDAN:21;
then
cl_Ball (hp,(s / 2)) c= Q
by A45, A49;
then
CLB c= h .: IU
by A43, XBOOLE_1:26, A40;
then A52:
hCLB c= IU
by RELAT_1:143, A37;
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 A35, XBOOLE_1:1;
Ball (hp,(s / 2)) c= Q
by A45, A49, A47, A51;
then
BB c= h .: IU
by XBOOLE_1:26, A40;
then A53:
h " BB c= IU
by RELAT_1:143, A37;
reconsider HCLB = hCLB as non empty Subset of M by A35, XBOOLE_1:1;
A54:
h .: hCLB = CLB
by A48, FUNCT_1:77;
A55:
((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 A43, PRE_TOPC:7;
A56:
(M | U) | hCLB = M | HCLB
by A35, 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 A55, A54, JORDAN24:12;
A57:
Int W c= W
by TOPS_1:16;
A58:
[#] (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, A32, XBOOLE_0:def 4, XBOOLE_1:1, A57, A42, TSEP_1:9;
A59:
IU c= W
by A57, A42;
then reconsider hCLW = hCLB as non empty Subset of (M | W) by A52, XBOOLE_1:1, A58;
A60:
(M | W) | hCLW = M | HCLB
by A52, A59, XBOOLE_1:1, PRE_TOPC:7;
set ghCLW = g .: hCLW;
A61:
[#] ((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;
A62:
((TOP-REAL n) | (Ball ((0. (TOP-REAL n)),1))) | (g .: hCLW) = (TOP-REAL n) | GhCLW
by A61, PRE_TOPC:7;
then reconsider g1 = g | hCLB as Function of (M | HCLB),((TOP-REAL n) | GhCLW) by A60, JORDAN24:12;
A63:
g1 is being_homeomorphism
by A33, METRIZTS:2, A62, A60;
then A64:
g1 " is being_homeomorphism
by TOPS_2:56;
A65:
dom g = [#] (M | W)
by A33, TOPS_2:def 5;
then
g . p in GhCLW
by A50, FUNCT_1:def 6;
then reconsider gp = g . p as Point of (TOP-REAL n) ;
(Int U) /\ (Int W) c= W
by A57, A42;
then reconsider hBW = hBB as Subset of (M | W) by A53, XBOOLE_1:1, A58;
reconsider ghBW = g .: hBW as Subset of (TOP-REAL n) by A61, XBOOLE_1:1;
hp in BB
by A46, A38, XBOOLE_0:def 4;
then
p in h " BB
by A36, A35, A34, A30, FUNCT_1:def 7;
then A66:
gp in ghBW
by A65, FUNCT_1:def 6;
set hg = h1 * (g1 ");
h1 is being_homeomorphism
by A28, A55, METRIZTS:2, A56, A54;
then A67:
h1 * (g1 ") is being_homeomorphism
by A64, TOPS_2:57;
then A68:
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, A43;
then A69:
hBB c= hCLB
by RELAT_1:143;
then
ghBW c= GhCLW
by RELAT_1:123;
then
gp in GhCLW
by A66;
then A70:
gp in dom (h1 * (g1 "))
by A68, 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 A46, A38, XBOOLE_0:def 4, PRE_TOPC:def 2;
then
h " BB is open
by A28, TOPGRP_1:26;
then
hBB is open
by A53, TSEP_1:9;
then
hBW is open
by TSEP_1:9;
then
g .: hBW is open
by A33, TOPGRP_1:25;
then
ghBW is open
by A61, TSEP_1:9;
then
gp in Int GhCLW
by A66, TOPS_1:22, A69, RELAT_1:123;
then A71:
(h1 * (g1 ")) . gp in Int ((cl_Ball (hp,(s / 2))) /\ (cl_Ball ((0. (TOP-REAL n)),1)))
by BROUWER3:11, A67;
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 A72:
(h1 * (g1 ")) . gp in Int (cl_Ball ((0. (TOP-REAL n)),1))
by A71, 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 A73:
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;
A74:
G1 " = g1 "
by A63, TOPS_2:def 4;
dom g1 = [#] (M | HCLB)
by A63, TOPS_2:def 5;
then
p in dom g1
by PRE_TOPC:def 5, A50;
then A75:
(g1 ") . (g1 . p) = p
by A63, A74, FUNCT_1:34;
A76:
g . p = g1 . p
by A50, FUNCT_1:49;
then A77:
p in dom h1
by A70, FUNCT_1:11, A75;
(h1 * (g1 ")) . gp = h1 . p
by A70, FUNCT_1:12, A75, A76;
then
(h1 * (g1 ")) . gp = h . p
by A77, FUNCT_1:47;
hence
contradiction
by A29, A72, A73, XBOOLE_0:def 5; verum