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 X 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 X 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 X holds h . x = max ((f . x),(g . x))
defpred S1[ set ] means f . $1 >= g . $1;
consider A being Subset of X 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 X 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 X holds h . x = max ((f . x),(g . x))
set h = the continuous Function of X,R;
take the continuous Function of X,R ; :: thesis: for x being Point of X holds the continuous Function of X,R . x = max ((f . x),(g . x))
let x be Point of X; :: thesis: the continuous Function of X,R . x = max ((f . x),(g . x))
A4: f . x = 0 by A3;
A5: g . x = 0 by A3;
thus the continuous Function of X,R . x = max ((f . x),(g . x)) by A3, A4, A5; :: 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 X holds h . x = max ((f . x),(g . x))
take g ; :: thesis: for x being Point of X holds g . x = max ((f . x),(g . x))
let x be Point of X; :: 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 X holds h . x = max ((f . x),(g . x))
take f ; :: thesis: for x being Point of X holds f . x = max ((f . x),(g . x))
let x be Point of X; :: 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 X holds h . x = max ((f . x),(g . x))
then reconsider X9 = X as non empty TopSpace ;
for x being Point of X9 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 A9 = A, B9 = B as non empty closed Subset of X9 by A8, Th49;
reconsider ff = f, gg = g as continuous Function of X9,R ;
A9: the carrier of (X9 | A9) = [#] (X9 | A9)
.= A9 by PRE_TOPC:def 5 ;
A10: dom ff = the carrier of X9 by FUNCT_2:def 1;
then dom (ff | A9) = A9 by RELAT_1:62;
then reconsider f9 = ff | A9 as continuous Function of (X9 | A9),R by A9, FUNCT_2:def 1, RELSET_1:18, TOPMETR:7;
A11: the carrier of (X9 | B9) = [#] (X9 | B9)
.= B9 by PRE_TOPC:def 5 ;
A12: dom gg = the carrier of X9 by FUNCT_2:def 1;
then dom (gg | B9) = B9 by RELAT_1:62;
then reconsider g9 = gg | B9 as continuous Function of (X9 | B9),R by A11, FUNCT_2:def 1, RELSET_1:18, TOPMETR:7;
A13: dom g9 = B by A12, RELAT_1:62;
A14: A9 \/ B9 = the carrier of X9
proof
thus A9 \/ B9 c= the carrier of X9 ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of X9 c= A9 \/ B9
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in the carrier of X9 or a in A9 \/ B9 )
reconsider aa = a as set by TARSKI:1;
( f . aa >= g . aa or f . aa <= g . aa ) ;
then ( not a in the carrier of X or a in A9 or a in B9 ) by A1, A2;
hence ( not a in the carrier of X9 or a in A9 \/ B9 ) by XBOOLE_0:def 3; :: thesis: verum
end;
then A15: X9 | (A9 \/ B9) = X9 | ([#] X9)
.= TopStruct(# the carrier of X, the topology of X #) by TSEP_1:93 ;
A16: TopStruct(# the carrier of R, the topology of R #) = TopStruct(# the carrier of R, the topology of R #) ;
A17: dom f9 = A by A10, RELAT_1:62;
A18: f9 tolerates g9
proof
let a be object ; :: according to PARTFUN1:def 4 :: thesis: ( not a in (proj1 f9) /\ (proj1 g9) or f9 . a = g9 . a )
assume A19: a in (dom f9) /\ (dom g9) ; :: thesis: f9 . a = g9 . 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 f9 . a = g . a by A20, FUNCT_1:49
.= g9 . a by A22, FUNCT_1:49 ;
:: thesis: verum
end;
then f9 +* g9 is continuous Function of (X9 | (A9 \/ B9)),R by Th10;
then reconsider h = f9 +* g9 as continuous Function of X,R by A16, A15, YELLOW12:36;
take h ; :: thesis: for x being Point of X holds h . x = max ((f . x),(g . x))
let x be Point of X; :: thesis: h . x = max ((f . x),(g . x))
( x in A9 or x in B9 ) by A14, XBOOLE_0:def 3;
then ( ( x in A9 & f . x >= g . x & h . x = f9 . x & f . x = f9 . x ) or ( x in B9 & f . x <= g . x & h . x = g9 . x & g . x = g9 . x ) ) by A1, A17, A13, A18, FUNCT_1:49, FUNCT_4:13, FUNCT_4:15;
hence h . x = max ((f . x),(g . x)) by XXREAL_0:def 10; :: thesis: verum
end;
end;