let n be Nat; for p being Point of (TOP-REAL n)
for A, B being Subset of (TOP-REAL n) st B is closed & p in Int A holds
for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds
h . p in Int B
let p be Point of (TOP-REAL n); for A, B being Subset of (TOP-REAL n) st B is closed & p in Int A holds
for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds
h . p in Int B
let A, B be Subset of (TOP-REAL n); ( B is closed & p in Int A implies for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds
h . p in Int B )
set TRn = TOP-REAL n;
set T = Tunit_circle n;
assume that
A1:
B is closed
and
A2:
p in Int A
; for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds
h . p in Int B
A3:
Int A c= A
by TOPS_1:16;
A4:
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n)
by EUCLID:def 8;
let h be Function of ((TOP-REAL n) | A),((TOP-REAL n) | B); ( h is being_homeomorphism implies h . p in Int B )
assume A5:
h is being_homeomorphism
; h . p in Int B
A6:
h " is continuous
by A5, TOPS_2:def 5;
A7:
[#] ((TOP-REAL n) | A) = A
by PRE_TOPC:def 5;
then A8:
dom h = A
by A5, TOPS_2:def 5;
A9:
[#] ((TOP-REAL n) | B) = B
by PRE_TOPC:def 5;
then A10:
rng h = B
by A5, TOPS_2:def 5;
per cases
( n = 0 or n > 0 )
;
suppose A11:
n > 0
;
h . p in Int BA12:
h . p in rng h
by A2, A3, A8, FUNCT_1:def 3;
then reconsider hp =
h . p as
Point of
(TOP-REAL n) by A10;
ex
r being
Real st
(
r > 0 & ( for
U being
open Subset of
((TOP-REAL n) | B) st
hp in U &
U c= Ball (
hp,
r) holds
ex
f being
Function of
((TOP-REAL n) | (B \ U)),
(Tunit_circle n) st
(
f is
continuous & ( for
h being
Function of
((TOP-REAL n) | B),
(Tunit_circle n) st
h is
continuous holds
h | (B \ U) <> f ) ) ) )
proof
reconsider hP =
hp as
Point of
(Euclid n) by A4, TOPMETR:12;
not
p in Fr A
by A2, TOPS_1:39, XBOOLE_0:3;
then consider r being
Real such that A14:
r > 0
and A15:
for
U being
open Subset of
((TOP-REAL n) | A) st
p in U &
U c= Ball (
p,
r) holds
ex
f being
Function of
((TOP-REAL n) | (A \ U)),
(Tunit_circle n) st
(
f is
continuous & ( for
h being
Function of
((TOP-REAL n) | A),
(Tunit_circle n) st
h is
continuous holds
h | (A \ U) <> f ) )
by A11, A2, A3, Th8;
reconsider BA =
(Ball (p,r)) /\ A as
Subset of
((TOP-REAL n) | A) by A7, XBOOLE_1:17;
Ball (
p,
r)
in the
topology of
(TOP-REAL n)
by PRE_TOPC:def 2;
then
BA in the
topology of
((TOP-REAL n) | A)
by A7, PRE_TOPC:def 4;
then reconsider BA =
BA as
open Subset of
((TOP-REAL n) | A) by PRE_TOPC:def 2;
h .: BA is
open
by A5, A2, A3, A12, TOPGRP_1:25;
then
h .: BA in the
topology of
((TOP-REAL n) | B)
by PRE_TOPC:def 2;
then consider U being
Subset of
(TOP-REAL n) such that A16:
U in the
topology of
(TOP-REAL n)
and A17:
h .: BA = U /\ ([#] ((TOP-REAL n) | B))
by PRE_TOPC:def 4;
reconsider U =
U as
open Subset of
(TOP-REAL n) by A16, PRE_TOPC:def 2;
A18:
Int U = U
by TOPS_1:23;
p is
Element of
REAL n
by EUCLID:22;
then
|.(p - p).| = 0
;
then
p in Ball (
p,
r)
by A14;
then
p in BA
by A2, A3, XBOOLE_0:def 4;
then
hp in h .: BA
by A7, A8, FUNCT_1:def 6;
then
hp in U
by A17, XBOOLE_0:def 4;
then consider s being
Real such that A19:
s > 0
and A20:
Ball (
hP,
s)
c= U
by A18, GOBOARD6:5;
take
s
;
( s > 0 & ( for U being open Subset of ((TOP-REAL n) | B) st hp in U & U c= Ball (hp,s) holds
ex f being Function of ((TOP-REAL n) | (B \ U)),(Tunit_circle n) st
( f is continuous & ( for h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st h is continuous holds
h | (B \ U) <> f ) ) ) )
thus
s > 0
by A19;
for U being open Subset of ((TOP-REAL n) | B) st hp in U & U c= Ball (hp,s) holds
ex f being Function of ((TOP-REAL n) | (B \ U)),(Tunit_circle n) st
( f is continuous & ( for h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st h is continuous holds
h | (B \ U) <> f ) )
let W be
open Subset of
((TOP-REAL n) | B);
( hp in W & W c= Ball (hp,s) implies ex f being Function of ((TOP-REAL n) | (B \ W)),(Tunit_circle n) st
( f is continuous & ( for h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st h is continuous holds
h | (B \ W) <> f ) ) )
assume that A21:
hp in W
and A22:
W c= Ball (
hp,
s)
;
ex f being Function of ((TOP-REAL n) | (B \ W)),(Tunit_circle n) st
( f is continuous & ( for h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st h is continuous holds
h | (B \ W) <> f ) )
A23:
W /\ B = W
by A9, XBOOLE_1:28;
Ball (
hp,
s)
= Ball (
hP,
s)
by TOPREAL9:13;
then
W c= U
by A22, A20;
then A24:
W c= U /\ B
by A23, XBOOLE_1:27;
h " (U /\ B) =
h " (h .: BA)
by A17, PRE_TOPC:def 5
.=
BA
by FUNCT_1:94, XBOOLE_1:17, A8, A5
;
then A25:
h " W c= BA
by A24, RELAT_1:143;
reconsider hW =
h " W as
open Subset of
((TOP-REAL n) | A) by TOPS_2:43, A5, A9, A12;
A26:
BA c= Ball (
p,
r)
by XBOOLE_1:17;
set BW =
B \ W;
reconsider bw =
B \ W as
Subset of
((TOP-REAL n) | B) by XBOOLE_1:36, A9;
A27:
[#] ((TOP-REAL n) | (A \ hW)) = A \ hW
by PRE_TOPC:def 5;
p in h " W
by A8, A2, A3, A21, FUNCT_1:def 7;
then consider F being
Function of
((TOP-REAL n) | (A \ hW)),
(Tunit_circle n) such that A28:
F is
continuous
and A29:
for
h being
Function of
((TOP-REAL n) | A),
(Tunit_circle n) st
h is
continuous holds
h | (A \ hW) <> F
by A15, A25, A26, XBOOLE_1:1;
A30:
B \ W c= B
by XBOOLE_1:36;
then A31:
(h ") .: (B \ W) =
h " (B \ W)
by TOPS_2:55, A9, A10, A5
.=
(h " B) \ hW
by FUNCT_1:69
.=
A \ hW
by RELAT_1:134, A8, A10
;
per cases
( A \ hW is empty or not A \ hW is empty )
;
suppose A34:
not
A \ hW is
empty
;
ex f being Function of ((TOP-REAL n) | (B \ W)),(Tunit_circle n) st
( f is continuous & ( for h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st h is continuous holds
h | (B \ W) <> f ) )reconsider hbw =
(h ") | (B \ W) as
Function of
(((TOP-REAL n) | B) | bw),
(((TOP-REAL n) | A) | ((h ") .: (B \ W))) by A2, A3, A12, JORDAN24:12;
A35:
((TOP-REAL n) | B) | bw = (TOP-REAL n) | (B \ W)
by PRE_TOPC:7, XBOOLE_1:36;
A36:
((TOP-REAL n) | A) | ((h ") .: (B \ W)) = (TOP-REAL n) | (A \ hW)
by A31, PRE_TOPC:7, A7;
then reconsider HBW =
hbw as
Function of
((TOP-REAL n) | (B \ W)),
((TOP-REAL n) | (A \ hW)) by A35;
reconsider fhW =
F * HBW as
Function of
((TOP-REAL n) | (B \ W)),
(Tunit_circle n) by A34;
take
fhW
;
( fhW is continuous & ( for h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st h is continuous holds
h | (B \ W) <> fhW ) )thus
fhW is
continuous
by A34, JORDAN24:13, A6, A2, A3, A12, A36, A35, A28, TOPS_2:46;
for h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st h is continuous holds
h | (B \ W) <> fhWlet g be
Function of
((TOP-REAL n) | B),
(Tunit_circle n);
( g is continuous implies g | (B \ W) <> fhW )assume A37:
g is
continuous
;
g | (B \ W) <> fhWreconsider gh =
g * h as
Function of
((TOP-REAL n) | A),
(Tunit_circle n) by A12;
A38:
gh is
continuous
by A5, A12, A37, TOPS_2:46;
assume A39:
g | (B \ W) = fhW
;
contradictionA40:
dom F = A \ hW
by FUNCT_2:def 1, A11, A27;
A41:
rng (h | (A \ hW)) =
h .: (A \ hW)
by RELAT_1:115
.=
h .: (h " (B \ W))
by TOPS_2:55, A9, A10, A31, A5, A30
.=
B \ W
by FUNCT_1:77, A10, XBOOLE_1:36
;
gh | (A \ hW) =
g * (h | (A \ hW))
by RELAT_1:83
.=
g * ((id (B \ W)) * (h | (A \ hW)))
by A41, RELAT_1:53
.=
(g * (id (B \ W))) * (h | (A \ hW))
by RELAT_1:36
.=
(g | (B \ W)) * (h | (A \ hW))
by RELAT_1:65
.=
F * (((h ") | (B \ W)) * (h | (A \ hW)))
by A39, RELAT_1:36
.=
F * (((h ") * (id (B \ W))) * (h | (A \ hW)))
by RELAT_1:65
.=
F * ((h ") * ((id (B \ W)) * (h | (A \ hW))))
by RELAT_1:36
.=
F * ((h ") * (h | (A \ hW)))
by A41, RELAT_1:53
.=
F * (((h ") * h) | (A \ hW))
by RELAT_1:83
.=
(F * ((h ") * h)) | (A \ hW)
by RELAT_1:83
.=
(F * (id A)) | (A \ hW)
by TOPS_2:52, A8, A10, A5, A9
.=
F | (dom F)
by A40, XBOOLE_1:36, RELAT_1:51
.=
F
;
hence
contradiction
by A38, A29;
verum end;
end; then
not
hp in Fr B
by A1, Th9;
then
hp in B \ (Fr B)
by A12, A9, XBOOLE_0:def 5;
hence
h . p in Int B
by TOPS_1:40;
verum end;