let n be Nat; for p being Point of (TOP-REAL n)
for A, B being Subset of (TOP-REAL n) st A is closed & p in Fr A holds
for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds
h . p in Fr B
let p be Point of (TOP-REAL n); for A, B being Subset of (TOP-REAL n) st A is closed & p in Fr A holds
for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds
h . p in Fr B
let A, B be Subset of (TOP-REAL n); ( A is closed & p in Fr A implies for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds
h . p in Fr B )
set TRn = TOP-REAL n;
assume that
A1:
A is closed
and
A2:
p in Fr A
; for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds
h . p in Fr B
A3:
Fr A c= A
by A1, TOPS_1:35;
let h be Function of ((TOP-REAL n) | A),((TOP-REAL n) | B); ( h is being_homeomorphism implies h . p in Fr B )
assume A4:
h is being_homeomorphism
; h . p in Fr B
A5:
[#] ((TOP-REAL n) | A) = A
by PRE_TOPC:def 5;
then A6:
dom h = A
by A4, TOPS_2:def 5;
then A7:
h . p in rng h
by A3, A2, FUNCT_1:def 3;
A8:
[#] ((TOP-REAL n) | B) = B
by PRE_TOPC:def 5;
then A9:
rng h = B
by A4, TOPS_2:def 5;
then reconsider hp = h . p as Point of (TOP-REAL n) by A7;
per cases
( n = 0 or n > 0 )
;
suppose A10:
n > 0
;
h . p in Fr Bthen reconsider n1 =
n - 1 as
Element of
NAT by NAT_1:20;
A11:
TopStruct(# the
carrier of
(TOP-REAL n), the
topology of
(TOP-REAL n) #)
= TopSpaceMetr (Euclid n)
by EUCLID:def 8;
for
r being
Real st
r > 0 holds
ex
U being
open Subset of
((TOP-REAL n) | B) st
(
hp in U &
U c= Ball (
hp,
r) & ( for
f being
Function of
((TOP-REAL n) | (B \ U)),
(Tunit_circle n) st
f is
continuous holds
ex
h being
Function of
((TOP-REAL n) | B),
(Tunit_circle n) st
(
h is
continuous &
h | (B \ U) = f ) ) )
proof
reconsider P =
p as
Point of
(Euclid n) by A11, TOPMETR:12;
let r be
Real;
( r > 0 implies ex U being open Subset of ((TOP-REAL n) | B) st
( hp in U & U c= Ball (hp,r) & ( for f being Function of ((TOP-REAL n) | (B \ U)),(Tunit_circle n) st f is continuous holds
ex h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st
( h is continuous & h | (B \ U) = f ) ) ) )
assume A13:
r > 0
;
ex U being open Subset of ((TOP-REAL n) | B) st
( hp in U & U c= Ball (hp,r) & ( for f being Function of ((TOP-REAL n) | (B \ U)),(Tunit_circle n) st f is continuous holds
ex h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st
( h is continuous & h | (B \ U) = f ) ) )
reconsider BB =
B /\ (Ball (hp,r)) as
Subset of
((TOP-REAL n) | B) by A8, XBOOLE_1:17;
Ball (
hp,
r)
in the
topology of
(TOP-REAL n)
by PRE_TOPC:def 2;
then
BB in the
topology of
((TOP-REAL n) | B)
by A8, PRE_TOPC:def 4;
then reconsider BB =
BB as
open Subset of
((TOP-REAL n) | B) by PRE_TOPC:def 2;
h " BB is
open
by A7, A4, A8, TOPS_2:43;
then
h " BB in the
topology of
((TOP-REAL n) | A)
by PRE_TOPC:def 2;
then consider U being
Subset of
(TOP-REAL n) such that A14:
U in the
topology of
(TOP-REAL n)
and A15:
h " BB = U /\ ([#] ((TOP-REAL n) | A))
by PRE_TOPC:def 4;
reconsider U =
U as
open Subset of
(TOP-REAL n) by A14, PRE_TOPC:def 2;
A16:
Int U = U
by TOPS_1:23;
hp is
Element of
REAL n
by EUCLID:22;
then
|.(hp - hp).| = 0
;
then
hp in Ball (
hp,
r)
by A13;
then
hp in BB
by A7, A8, XBOOLE_0:def 4;
then
p in h " BB
by A3, A2, A6, FUNCT_1:def 7;
then
p in U
by A15, XBOOLE_0:def 4;
then consider s being
Real such that A17:
s > 0
and A18:
Ball (
P,
s)
c= U
by A16, GOBOARD6:5;
consider W being
open Subset of
((TOP-REAL n) | A) such that A19:
p in W
and A20:
W c= Ball (
p,
s)
and A21:
for
f being
Function of
((TOP-REAL n) | (A \ W)),
(Tunit_circle n) st
f is
continuous holds
ex
h being
Function of
((TOP-REAL n) | A),
(Tunit_circle n) st
(
h is
continuous &
h | (A \ W) = f )
by A1, A17, Th9, A2;
Ball (
p,
s)
= Ball (
P,
s)
by TOPREAL9:13;
then A22:
(Ball (p,s)) /\ A c= U /\ A
by A18, XBOOLE_1:27;
W /\ A = W
by A5, XBOOLE_1:28;
then
W c= (Ball (p,s)) /\ A
by A20, XBOOLE_1:27;
then
W c= U /\ A
by A22;
then
h .: W c= h .: (U /\ A)
by RELAT_1:123;
then A23:
h .: W c= BB
by FUNCT_1:77, A8, A9, A15, A5;
not
(TOP-REAL n) | B is
empty
by A3, A2, A6;
then reconsider hW =
h .: W as
open Subset of
((TOP-REAL n) | B) by A3, A2, A4, TOPGRP_1:25;
take
hW
;
( hp in hW & hW c= Ball (hp,r) & ( for f being Function of ((TOP-REAL n) | (B \ hW)),(Tunit_circle n) st f is continuous holds
ex h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st
( h is continuous & h | (B \ hW) = f ) ) )
BB c= Ball (
hp,
r)
by XBOOLE_1:17;
hence
(
hp in hW &
hW c= Ball (
hp,
r) )
by A3, A2, A6, FUNCT_1:def 6, A19, A23;
for f being Function of ((TOP-REAL n) | (B \ hW)),(Tunit_circle n) st f is continuous holds
ex h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st
( h is continuous & h | (B \ hW) = f )
set AW =
A \ W;
set haw =
h | (A \ W);
set T =
Tunit_circle n;
A24:
[#] ((TOP-REAL n) | (B \ hW)) = B \ hW
by PRE_TOPC:def 5;
reconsider aw =
A \ W as
Subset of
((TOP-REAL n) | A) by XBOOLE_1:36, A5;
let f be
Function of
((TOP-REAL n) | (B \ hW)),
(Tunit_circle n);
( f is continuous implies ex h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st
( h is continuous & h | (B \ hW) = f ) )
assume A25:
f is
continuous
;
ex h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st
( h is continuous & h | (B \ hW) = f )
per cases
( B \ hW is empty or not B \ hW is empty )
;
suppose A27:
not
B \ hW is
empty
;
ex h being Function of ((TOP-REAL n) | B),(Tunit_circle n) st
( h is continuous & h | (B \ hW) = f )set AW =
A \ W;
set haw =
h | (A \ W);
set T =
Tunit_circle n;
reconsider haw =
h | (A \ W) as
Function of
(((TOP-REAL n) | A) | aw),
(((TOP-REAL n) | B) | (h .: (A \ W))) by A3, A2, A7, JORDAN24:12;
A28:
h .: (A \ W) =
(h .: A) \ (h .: W)
by A4, FUNCT_1:64
.=
B \ hW
by RELAT_1:113, A6, A9
;
then A29:
((TOP-REAL n) | B) | (h .: (A \ W)) = (TOP-REAL n) | (B \ hW)
by XBOOLE_1:36, PRE_TOPC:7;
A30:
((TOP-REAL n) | A) | aw = (TOP-REAL n) | (A \ W)
by PRE_TOPC:7, XBOOLE_1:36;
then reconsider HAW =
haw as
Function of
((TOP-REAL n) | (A \ W)),
((TOP-REAL n) | (B \ hW)) by A29;
reconsider fhW =
f * HAW as
Function of
((TOP-REAL n) | (A \ W)),
(Tunit_circle n) by A27;
fhW is
continuous
by A27, JORDAN24:13, A4, A3, A2, A7, A29, A30, A25, TOPS_2:46;
then consider HW being
Function of
((TOP-REAL n) | A),
(Tunit_circle n) such that A31:
HW is
continuous
and A32:
HW | (A \ W) = fhW
by A21;
reconsider HWh =
HW * (h ") as
Function of
((TOP-REAL n) | B),
(Tunit_circle n) by A3, A2;
take
HWh
;
( HWh is continuous & HWh | (B \ hW) = f )
h " is
continuous
by A4, TOPS_2:def 5;
hence
HWh is
continuous
by TOPS_2:46, A3, A2, A31;
HWh | (B \ hW) = fA33:
dom f = B \ hW
by A10, A24, FUNCT_2:def 1;
A34:
rng ((h ") | (B \ hW)) =
(h ") .: (B \ hW)
by RELAT_1:115
.=
h " (h .: (A \ W))
by A28, A8, A9, A4, TOPS_2:55
.=
A \ W
by FUNCT_1:94, A6, A4, XBOOLE_1:36
;
thus HWh | (B \ hW) =
HW * ((h ") | (B \ hW))
by RELAT_1:83
.=
HW * ((id (A \ W)) * ((h ") | (B \ hW)))
by A34, RELAT_1:53
.=
(HW * (id (A \ W))) * ((h ") | (B \ hW))
by RELAT_1:36
.=
(HW | (A \ W)) * ((h ") | (B \ hW))
by RELAT_1:65
.=
((f * h) | (A \ W)) * ((h ") | (B \ hW))
by A32, RELAT_1:83
.=
((f * h) * (id (A \ W))) * ((h ") | (B \ hW))
by RELAT_1:65
.=
(f * h) * ((id (A \ W)) * ((h ") | (B \ hW)))
by RELAT_1:36
.=
(f * h) * ((h ") | (B \ hW))
by A34, RELAT_1:53
.=
((f * h) * (h ")) | (B \ hW)
by RELAT_1:83
.=
(f * (h * (h "))) | (B \ hW)
by RELAT_1:36
.=
(f * (id B)) | (B \ hW)
by TOPS_2:52, A9, A4, A8
.=
f | (dom f)
by A33, XBOOLE_1:36, RELAT_1:51
.=
f
;
verum end;
end; hence
h . p in Fr B
by Th8, A7, A8, A10;
verum end;