let n be Nat; for T, S being TopSpace
for A being closed Subset of T
for B being Subset of S st T is normal holds
for X being Subset of (TOP-REAL n) st X is compact & not X is boundary & X is convex & B,X are_homeomorphic holds
for f being Function of (T | A),(S | B) st f is continuous holds
ex g being Function of T,(S | B) st
( g is continuous & g | A = f )
let T, S be TopSpace; for A being closed Subset of T
for B being Subset of S st T is normal holds
for X being Subset of (TOP-REAL n) st X is compact & not X is boundary & X is convex & B,X are_homeomorphic holds
for f being Function of (T | A),(S | B) st f is continuous holds
ex g being Function of T,(S | B) st
( g is continuous & g | A = f )
let A be closed Subset of T; for B being Subset of S st T is normal holds
for X being Subset of (TOP-REAL n) st X is compact & not X is boundary & X is convex & B,X are_homeomorphic holds
for f being Function of (T | A),(S | B) st f is continuous holds
ex g being Function of T,(S | B) st
( g is continuous & g | A = f )
let B be Subset of S; ( T is normal implies for X being Subset of (TOP-REAL n) st X is compact & not X is boundary & X is convex & B,X are_homeomorphic holds
for f being Function of (T | A),(S | B) st f is continuous holds
ex g being Function of T,(S | B) st
( g is continuous & g | A = f ) )
assume A1:
T is normal
; for X being Subset of (TOP-REAL n) st X is compact & not X is boundary & X is convex & B,X are_homeomorphic holds
for f being Function of (T | A),(S | B) st f is continuous holds
ex g being Function of T,(S | B) st
( g is continuous & g | A = f )
A2:
[#] (T | A) = A
by PRE_TOPC:def 5;
A3:
[#] (S | B) = B
by PRE_TOPC:def 5;
set TR = TOP-REAL n;
let X be Subset of (TOP-REAL n); ( X is compact & not X is boundary & X is convex & B,X are_homeomorphic implies for f being Function of (T | A),(S | B) st f is continuous holds
ex g being Function of T,(S | B) st
( g is continuous & g | A = f ) )
assume that
A4:
( X is compact & not X is boundary & X is convex )
and
A5:
B,X are_homeomorphic
; for f being Function of (T | A),(S | B) st f is continuous holds
ex g being Function of T,(S | B) st
( g is continuous & g | A = f )
consider h being Function of (S | B),((TOP-REAL n) | X) such that
A6:
h is being_homeomorphism
by METRIZTS:def 1, A5, T_0TOPSP:def 1;
A7:
h " is continuous
by TOPS_2:def 5, A6;
let f be Function of (T | A),(S | B); ( f is continuous implies ex g being Function of T,(S | B) st
( g is continuous & g | A = f ) )
assume A8:
f is continuous
; ex g being Function of T,(S | B) st
( g is continuous & g | A = f )
A9:
rng f c= the carrier of (S | B)
;
A10:
dom h = [#] (S | B)
by TOPS_2:def 5, A6;
A11:
not X is empty
by A4;
A12:
rng h = [#] ((TOP-REAL n) | X)
by TOPS_2:def 5, A6;
then A13:
not B is empty
by A11;
per cases
( A is empty or not A is empty )
;
suppose A15:
not
A is
empty
;
ex g being Function of T,(S | B) st
( g is continuous & g | A = f )reconsider hf =
h * f as
Function of
(T | A),
((TOP-REAL n) | X) by A3, A13;
consider g being
Function of
T,
((TOP-REAL n) | X) such that A16:
g is
continuous
and A17:
g | A = hf
by A3, A13, A2, A11, A15, A8, A6, A1, A4, Th23;
reconsider hg =
(h ") * g as
Function of
T,
(S | B) by A11;
take
hg
;
( hg is continuous & hg | A = f )hg | A =
(h ") * (g | A)
by RELAT_1:83
.=
((h ") * h) * f
by A17, RELAT_1:36
.=
(id (dom h)) * f
by TOPS_2:52, A12, A6
.=
f
by A10, A9, RELAT_1:53
;
hence
(
hg is
continuous &
hg | A = f )
by A7, A11, A16, TOPS_2:46;
verum end; end;