let X be TopSpace; :: thesis: for R being non empty SubSpace of R^1
for f, g being continuous Function of X,R ex h being continuous Function of X,R st
for x being Point of holds h . x = max (f . x),(g . x)
let R be non empty SubSpace of R^1 ; :: thesis: for f, g being continuous Function of X,R ex h being continuous Function of X,R st
for x being Point of holds h . x = max (f . x),(g . x)
let f, g be continuous Function of X,R; :: thesis: ex h being continuous Function of X,R st
for x being Point of holds h . x = max (f . x),(g . x)
defpred S1[ set ] means f . $1 >= g . $1;
consider A being Subset of such that
A1: for a being set holds
( a in A iff ( a in the carrier of X & S1[a] ) ) from SUBSET_1:sch 1();
 defpred S2[ set ] means f . $1 <= g . $1;
consider B being Subset of such that
A2: for a being set holds
( a in B iff ( a in the carrier of X & S2[a] ) ) from SUBSET_1:sch 1();
per cases ( X is empty or ( not X is empty & A is empty ) or ( not X is empty & B is empty ) or ( not X is empty & not A is empty & not B is empty ) ) ;
suppose A3: X is empty ; :: thesis: ex h being continuous Function of X,R st
for x being Point of holds h . x = max (f . x),(g . x)
consider h being continuous Function of X,R;
take h ; :: thesis: for x being Point of holds h . x = max (f . x),(g . x)
let x be Point of ; :: thesis: h . x = max (f . x),(g . x)
dom f = the carrier of X by FUNCT_2:def 1;
then A4: f . x = 0 by A3, FUNCT_1:def 4;
dom g = the carrier of X by FUNCT_2:def 1;
then A5: g . x = 0 by A3, FUNCT_1:def 4;
dom h = the carrier of X by FUNCT_2:def 1;
hence h . x = max (f . x),(g . x) by A3, A4, A5, FUNCT_1:def 4; :: thesis: verum
end;
suppose A6: ( not X is empty & A is empty ) ; :: thesis: ex h being continuous Function of X,R st
for x being Point of holds h . x = max (f . x),(g . x)
take g ; :: thesis: for x being Point of holds g . x = max (f . x),(g . x)
let x be Point of ; :: thesis: g . x = max (f . x),(g . x)
f . x < g . x by A6, A1;
hence g . x = max (f . x),(g . x) by XXREAL_0:def 10; :: thesis: verum
end;
suppose A7: ( not X is empty & B is empty ) ; :: thesis: ex h being continuous Function of X,R st
for x being Point of holds h . x = max (f . x),(g . x)
take f ; :: thesis: for x being Point of holds f . x = max (f . x),(g . x)
let x be Point of ; :: thesis: f . x = max (f . x),(g . x)
g . x < f . x by A7, A2;
hence f . x = max (f . x),(g . x) by XXREAL_0:def 10; :: thesis: verum
end;
suppose A8: ( not X is empty & not A is empty & not B is empty ) ; :: thesis: ex h being continuous Function of X,R st
for x being Point of holds h . x = max (f . x),(g . x)
then reconsider X' = X as non empty TopSpace ;
for x being Point of holds
( ( x in A implies f . x >= g . x ) & ( f . x >= g . x implies x in A ) & ( x in B implies f . x <= g . x ) & ( f . x <= g . x implies x in B ) ) by A1, A2;
then reconsider A' = A, B' = B as non empty closed Subset of by A8, Th53;
reconsider ff = f, gg = g as continuous Function of X',R ;
A9: the carrier of (X' | A') = [#] (X' | A')
.= A' by PRE_TOPC:def 10 ;
A10: dom ff = the carrier of X' by FUNCT_2:def 1;
then dom (ff | A') = A' by RELAT_1:91;
then reconsider f' = ff | A' as continuous Function of (X' | A'),R by A9, FUNCT_2:def 1, RELSET_1:33, TOPMETR:10;
A11: the carrier of (X' | B') = [#] (X' | B')
.= B' by PRE_TOPC:def 10 ;
A12: dom gg = the carrier of X' by FUNCT_2:def 1;
then dom (gg | B') = B' by RELAT_1:91;
then reconsider g' = gg | B' as continuous Function of (X' | B'),R by A11, FUNCT_2:def 1, RELSET_1:33, TOPMETR:10;
A13: dom g' = B by A12, RELAT_1:91;
A14: A' \/ B' = the carrier of X'
proof
thus A' \/ B' c= the carrier of X' ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of X' c= A' \/ B'
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of X' or a in A' \/ B' )
( f . a >= g . a or f . a <= g . a ) ;
then ( not a in the carrier of X or a in A' or a in B' ) by A1, A2;
hence ( not a in the carrier of X' or a in A' \/ B' ) by XBOOLE_0:def 3; :: thesis: verum
end;
then A15: X' | (A' \/ B') = X' | ([#] X')
.= TopStruct(# the carrier of X,the topology of X #) by TSEP_1:100 ;
A16: TopStruct(# the carrier of R,the topology of R #) = TopStruct(# the carrier of R,the topology of R #) ;
A17: dom f' = A by A10, RELAT_1:91;
A18: f' tolerates g'
proof
let a be set ; :: according to PARTFUN1:def 6 :: thesis: ( not a in (proj1 f') /\ (proj1 g') or f' . a = g' . a )
assume A19: a in (dom f') /\ (dom g') ; :: thesis: f' . a = g' . a
then A20: a in A by A17, XBOOLE_0:def 4;
then A21: f . a >= g . a by A1;
A22: a in B by A19, A13, XBOOLE_0:def 4;
then f . a <= g . a by A2;
then f . a = g . a by A21, XXREAL_0:1;
hence f' . a = g . a by A20, FUNCT_1:72
.= g' . a by A22, FUNCT_1:72 ;
:: thesis: verum
end;
then f' +* g' is continuous Function of (X' | (A' \/ B')),R by Th14;
then reconsider h = f' +* g' as continuous Function of X,R by A16, A15, YELLOW12:36;
take h ; :: thesis: for x being Point of holds h . x = max (f . x),(g . x)
let x be Point of ; :: thesis: h . x = max (f . x),(g . x)
( x in A' or x in B' ) by A14, XBOOLE_0:def 3;
then ( ( x in A' & f . x >= g . x & h . x = f' . x & f . x = f' . x ) or ( x in B' & f . x <= g . x & h . x = g' . x & g . x = g' . x ) ) by A1, A2, A17, A13, A18, FUNCT_1:72, FUNCT_4:14, FUNCT_4:16;
hence h . x = max (f . x),(g . x) by XXREAL_0:def 10; :: thesis: verum
end;
end;