let n be Nat; for A being Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) st p in Fr A & A is closed holds
for r being Real st r > 0 holds
ex U being open Subset of ((TOP-REAL n) | A) st
( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(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 \ U) = f ) ) )
let A be Subset of (TOP-REAL n); for p being Point of (TOP-REAL n) st p in Fr A & A is closed holds
for r being Real st r > 0 holds
ex U being open Subset of ((TOP-REAL n) | A) st
( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(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 \ U) = f ) ) )
set TR = TOP-REAL n;
let p be Point of (TOP-REAL n); ( p in Fr A & A is closed implies for r being Real st r > 0 holds
ex U being open Subset of ((TOP-REAL n) | A) st
( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(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 \ U) = f ) ) ) )
assume that
A1:
p in Fr A
and
A2:
A is closed
; for r being Real st r > 0 holds
ex U being open Subset of ((TOP-REAL n) | A) st
( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(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 \ U) = f ) ) )
A3:
Fr A c= A
by TOPS_1:35, A2;
n > 0
then reconsider n1 = n - 1 as Element of NAT by NAT_1:20;
set TU = Tunit_circle n;
A5:
p is Element of REAL n
by EUCLID:22;
let r be Real; ( r > 0 implies ex U being open Subset of ((TOP-REAL n) | A) st
( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(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 \ U) = f ) ) ) )
assume A6:
r > 0
; ex U being open Subset of ((TOP-REAL n) | A) st
( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(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 \ U) = f ) ) )
set r3 = r / 3;
set r2 = 2 * (r / 3);
set B = Ball (p,(r / 3));
p is Element of REAL n
by EUCLID:22;
then
|.(p - p).| = 0
;
then
p in Ball (p,(r / 3))
by A6;
then
A ` meets Ball (p,(r / 3))
by A1, TOPS_1:28;
then consider x being object such that
A7:
x in A `
and
A8:
x in Ball (p,(r / 3))
by XBOOLE_0:3;
reconsider x = x as Element of (TOP-REAL n) by A7;
set u = Ball (x,(2 * (r / 3)));
set clU = cl_Ball (x,(2 * (r / 3)));
A9:
n in NAT
by ORDINAL1:def 12;
A10:
Ball (x,(2 * (r / 3))) c= cl_Ball (x,(2 * (r / 3)))
by TOPREAL9:16;
A11:
[#] ((TOP-REAL n) | A) = A
by PRE_TOPC:def 5;
then reconsider U = (Ball (x,(2 * (r / 3)))) /\ A as Subset of ((TOP-REAL n) | A) by XBOOLE_1:17;
Ball (x,(2 * (r / 3))) in the topology of (TOP-REAL n)
by PRE_TOPC:def 2;
then
U in the topology of ((TOP-REAL n) | A)
by PRE_TOPC:def 4, A11;
then reconsider U = U as open Subset of ((TOP-REAL n) | A) by PRE_TOPC:def 2;
take
U
; ( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(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 \ U) = f ) ) )
x is Element of REAL n
by EUCLID:22;
then A12:
|.(x - p).| = |.(p - x).|
by EUCLID:18, A5;
|.(x - p).| + (2 * (r / 3)) < (r / 3) + (2 * (r / 3))
by A8, TOPREAL9:7, XREAL_1:6;
then A13:
Ball (x,(2 * (r / 3))) c= Ball (p,r)
by Th5;
2 * (r / 3) > r / 3
by A6, XREAL_1:155;
then
|.(x - p).| < 2 * (r / 3)
by A8, TOPREAL9:7, XXREAL_0:2;
then A14:
p in Ball (x,(2 * (r / 3)))
by A12;
hence
p in U
by A3, A1, XBOOLE_0:def 4; ( U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(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 \ U) = f ) ) )
U c= Ball (x,(2 * (r / 3)))
by XBOOLE_1:17;
hence
U c= Ball (p,r)
by A13; for f being Function of ((TOP-REAL n) | (A \ U)),(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 \ U) = f )
let f be Function of ((TOP-REAL n) | (A \ U)),(Tunit_circle n); ( f is continuous implies ex h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st
( h is continuous & h | (A \ U) = f ) )
assume A15:
f is continuous
; ex h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st
( h is continuous & h | (A \ U) = f )
per cases
( A \ U is empty or not A \ U is empty )
;
suppose A17:
not
A \ U is
empty
;
ex h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st
( h is continuous & h | (A \ U) = f )set S =
Sphere (
x,
(2 * (r / 3)));
reconsider AUS =
(A \ U) \/ (Sphere (x,(2 * (r / 3)))) as non
empty Subset of
(TOP-REAL n) by A17;
A18:
(
(TOP-REAL n) | AUS is
metrizable &
(TOP-REAL n) | AUS is
finite-ind &
(TOP-REAL n) | AUS is
second-countable )
A20:
[#] ((TOP-REAL n) | AUS) = AUS
by PRE_TOPC:def 5;
then reconsider AU =
A \ U,
SS =
Sphere (
x,
(2 * (r / 3))) as
Subset of
((TOP-REAL n) | AUS) by XBOOLE_1:7;
AU ` =
AUS \ AU
by SUBSET_1:def 4, A20
.=
(Sphere (x,(2 * (r / 3)))) \ AU
by XBOOLE_1:40
;
then A21:
AU ` c= SS
by XBOOLE_1:36;
ind (Sphere (x,(2 * (r / 3)))) = n1
by A6, Th7;
then
ind SS = n1
by TOPDIM_1:21;
then A22:
ind (AU `) <= n1
by TOPDIM_1:19, A21;
A23:
(TOP-REAL n) | (A \ U) = ((TOP-REAL n) | AUS) | AU
by A20, PRE_TOPC:7;
then reconsider F =
f as
Function of
(((TOP-REAL n) | AUS) | AU),
(Tunit_circle n) ;
A \ U = A \ (Ball (x,(2 * (r / 3))))
by XBOOLE_1:47;
then A24:
A \ U is
closed
by A2, YELLOW_8:20;
then
AU is
closed
by TSEP_1:8;
then consider g being
continuous Function of
((TOP-REAL n) | AUS),
(Tunit_circle (n1 + 1)) such that A25:
g | AU = F
by Th3, A23, A15, A18, A22;
A26:
[#] ((TOP-REAL n) | A) = A
by PRE_TOPC:def 5;
then reconsider AclU =
A /\ (cl_Ball (x,(2 * (r / 3)))),
au =
A \ U as
Subset of
((TOP-REAL n) | A) by XBOOLE_1:17, XBOOLE_1:36;
set T3 =
((TOP-REAL n) | A) | AclU;
set T4 =
((TOP-REAL n) | A) | au;
A27:
(A /\ U) \/ au = A
by XBOOLE_1:51;
A ` = ([#] (TOP-REAL n)) \ A
by SUBSET_1:def 4;
then
not
x in A
by A7, XBOOLE_0:def 5;
then consider h being
Function of
((TOP-REAL n) | A),
((TOP-REAL n) | (Sphere (x,(2 * (r / 3))))) such that A28:
h is
continuous
and A29:
h | (Sphere (x,(2 * (r / 3)))) = id (A /\ (Sphere (x,(2 * (r / 3)))))
by A6, Th4;
A30:
n1 + 1
= n
;
then A31:
dom h = the
carrier of
((TOP-REAL n) | A)
by A6, FUNCT_2:def 1;
A32:
[#] ((TOP-REAL n) | (Sphere (x,(2 * (r / 3))))) = Sphere (
x,
(2 * (r / 3)))
by PRE_TOPC:def 5;
then
rng h c= the
carrier of
(TOP-REAL n)
by XBOOLE_1:1;
then reconsider h1 =
h as
Function of
((TOP-REAL n) | A),
(TOP-REAL n) by A31, FUNCT_2:2;
A33:
Sphere (
x,
(2 * (r / 3)))
c= AUS
by XBOOLE_1:7;
rng h c= [#] ((TOP-REAL n) | (Sphere (x,(2 * (r / 3)))))
;
then reconsider h2 =
h1 as
Function of
((TOP-REAL n) | A),
((TOP-REAL n) | AUS) by A33, A32, XBOOLE_1:1, A31, FUNCT_2:2, A20;
h1 is
continuous
by A28, PRE_TOPC:26;
then A34:
h2 is
continuous
by PRE_TOPC:27;
set T2 =
((TOP-REAL n) | AUS) | AU;
A35:
((TOP-REAL n) | AUS) | AU = (TOP-REAL n) | (A \ U)
by PRE_TOPC:7, XBOOLE_1:7;
A36:
(cl_Ball (x,(2 * (r / 3)))) \ (Ball (x,(2 * (r / 3)))) = Sphere (
x,
(2 * (r / 3)))
by JORDAN:19, A9;
A37:
(A /\ A) /\ (Ball (x,(2 * (r / 3)))) = A /\ (A /\ (Ball (x,(2 * (r / 3)))))
by XBOOLE_1:16;
A38:
g | (((TOP-REAL n) | AUS) | AU) = g | the
carrier of
(((TOP-REAL n) | AUS) | AU)
by TMAP_1:def 4;
((TOP-REAL n) | A) | au = (TOP-REAL n) | (A \ U)
by XBOOLE_1:36, PRE_TOPC:7;
then reconsider gT2 =
g | (((TOP-REAL n) | AUS) | AU) as
continuous Function of
(((TOP-REAL n) | A) | au),
(Tunit_circle (n1 + 1)) by A35, A17;
A39:
[#] (((TOP-REAL n) | A) | AclU) = AclU
by PRE_TOPC:def 5;
not
AclU is
empty
by A10, A14, A3, A1, XBOOLE_0:def 4;
then reconsider gh2T3 =
g * (h2 | (((TOP-REAL n) | A) | AclU)) as
continuous Function of
(((TOP-REAL n) | A) | AclU),
(Tunit_circle (n1 + 1)) by A34;
A40:
[#] (((TOP-REAL n) | A) | au) = au
by PRE_TOPC:def 5;
A41:
h2 | (((TOP-REAL n) | A) | AclU) = h2 | the
carrier of
(((TOP-REAL n) | A) | AclU)
by A3, A1, TMAP_1:def 4;
A42:
now for x being object st x in (dom gh2T3) /\ (dom gT2) holds
gh2T3 . x = gT2 . xlet x be
object ;
( x in (dom gh2T3) /\ (dom gT2) implies gh2T3 . x = gT2 . x )assume A43:
x in (dom gh2T3) /\ (dom gT2)
;
gh2T3 . x = gT2 . xA44:
not
x in U
by A43, A40, XBOOLE_0:def 5;
x in A
by A43, A40, XBOOLE_0:def 5;
then A45:
not
x in Ball (
x,
(2 * (r / 3)))
by A44, XBOOLE_0:def 4;
A46:
x in dom gh2T3
by A43, XBOOLE_0:def 4;
then
x in cl_Ball (
x,
(2 * (r / 3)))
by A39, XBOOLE_0:def 4;
then A47:
x in Sphere (
x,
(2 * (r / 3)))
by A45, A36, XBOOLE_0:def 5;
A48:
x in dom gT2
by A43, XBOOLE_0:def 4;
x in A
by A46, A39, XBOOLE_0:def 4;
then A49:
x in A /\ (Sphere (x,(2 * (r / 3))))
by A47, XBOOLE_0:def 4;
x in dom (h2 | (((TOP-REAL n) | A) | AclU))
by A46, FUNCT_1:11;
then (h2 | (((TOP-REAL n) | A) | AclU)) . x =
h2 . x
by A41, FUNCT_1:47
.=
(h | (Sphere (x,(2 * (r / 3))))) . x
by A47, FUNCT_1:49
.=
x
by A29, A49, FUNCT_1:17
;
hence gh2T3 . x =
g . x
by A46, FUNCT_1:12
.=
gT2 . x
by A38, A48, FUNCT_1:47
;
verum end; A50:
AclU is
closed
by A2, TSEP_1:8;
au is
closed
by A24, TSEP_1:8;
then reconsider G =
gh2T3 +* gT2 as
continuous Function of
(((TOP-REAL n) | A) | (AclU \/ au)),
(Tunit_circle (n1 + 1)) by A50, A42, PARTFUN1:def 4, TOPGEN_5:10;
W:
A /\ (Ball (x,(2 * (r / 3)))) c= AclU
by TOPREAL9:16, XBOOLE_1:26;
A = AclU \/ au
by A26, W, A27, A37, XBOOLE_1:9;
then A51:
((TOP-REAL n) | A) | (AclU \/ au) = (TOP-REAL n) | A
by A26, TSEP_1:93;
then reconsider GG =
G as
Function of
((TOP-REAL n) | A),
(Tunit_circle n) ;
take
GG
;
( GG is continuous & GG | (A \ U) = f )thus
GG is
continuous
by A51;
GG | (A \ U) = fA52:
[#] ((TOP-REAL n) | (A \ U)) = A \ U
by PRE_TOPC:def 5;
A53:
dom gT2 = the
carrier of
(((TOP-REAL n) | A) | au)
by FUNCT_2:def 1;
A54:
now for x being set st x in dom f holds
(GG | (A \ U)) . x = f . xlet x be
set ;
( x in dom f implies (GG | (A \ U)) . x = f . x )assume A55:
x in dom f
;
(GG | (A \ U)) . x = f . xhence (GG | (A \ U)) . x =
GG . x
by A52, FUNCT_1:49
.=
gT2 . x
by FUNCT_4:13, A55, A52, A40, A53
.=
g . x
by A38, A40, A52, A53, A55, FUNCT_1:47
.=
f . x
by A25, A55, A52, FUNCT_1:49
;
verum end;
dom GG = A
by A26, FUNCT_2:def 1;
then A56:
dom (GG | (A \ U)) =
A /\ (A \ U)
by RELAT_1:61
.=
A \ U
by XBOOLE_1:36, XBOOLE_1:28
;
dom f = A \ U
by A30, A52, FUNCT_2:def 1;
hence
GG | (A \ U) = f
by A54, A56;
verum end;