let X be TopSpace; 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 ; 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; 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
;
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
;
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;
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;
verum end; suppose A8:
( not
X is
empty & not
A is
empty & not
B is
empty )
;
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
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
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
;
for x being Point of X holds h . x = max ((f . x),(g . x))let x be
Point of
X;
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;
verum end; end;