let n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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); :: thesis: ( f is continuous implies ex g being Function of T,(S | B) st
( g is continuous & g | A = f ) )
assume A8: f is continuous ; :: thesis: 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 A14: A is empty ; :: thesis: ex g being Function of T,(S | B) st
( g is continuous & g | A = f )
reconsider SB = S | B as non empty TopSpace by A11, A12;
set h = the continuous Function of T,SB;
reconsider h = the continuous Function of T,SB as Function of T,(S | B) ;
take h ; :: thesis: ( h is continuous & h | A = f )
f = {} by A14;
hence ( h is continuous & h | A = f ) by A14; :: thesis: verum
end;
suppose A15: not A is empty ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: verum
end;
end;