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