let X be non empty TopSpace; for R being non empty SubSpace of R^1
for A being non empty finite set
for F being ManySortedFunction of A st ( for a being set st a in A holds
F . a is continuous Function of X,R ) holds
ex f being continuous Function of X,R st
for x being Point of X
for S being non empty finite Subset of REAL st S = rng ((commute F) . x) holds
f . x = max S
let R be non empty SubSpace of R^1 ; for A being non empty finite set
for F being ManySortedFunction of A st ( for a being set st a in A holds
F . a is continuous Function of X,R ) holds
ex f being continuous Function of X,R st
for x being Point of X
for S being non empty finite Subset of REAL st S = rng ((commute F) . x) holds
f . x = max S
let A be non empty finite set ; for F being ManySortedFunction of A st ( for a being set st a in A holds
F . a is continuous Function of X,R ) holds
ex f being continuous Function of X,R st
for x being Point of X
for S being non empty finite Subset of REAL st S = rng ((commute F) . x) holds
f . x = max S
let F be ManySortedFunction of A; ( ( for a being set st a in A holds
F . a is continuous Function of X,R ) implies ex f being continuous Function of X,R st
for x being Point of X
for S being non empty finite Subset of REAL st S = rng ((commute F) . x) holds
f . x = max S )
defpred S1[ set ] means ( $1 is empty or ex f being continuous Function of X,R st
for x being Point of X
for S being non empty finite Subset of REAL st S = rng ((commute (F | $1)) . x) holds
f . x = max S );
A1:
S1[ {} ]
;
A2:
dom F = A
by PARTFUN1:def 2;
assume A3:
for a being set st a in A holds
F . a is continuous Function of X,R
; ex f being continuous Function of X,R st
for x being Point of X
for S being non empty finite Subset of REAL st S = rng ((commute F) . x) holds
f . x = max S
rng F c= Funcs ( the carrier of X, the carrier of R)
then A4:
F in Funcs (A,(Funcs ( the carrier of X, the carrier of R)))
by A2, FUNCT_2:def 2;
A5:
now for x, B being set st x in A & B c= A & S1[B] holds
S1[B \/ {x}]let x,
B be
set ;
( x in A & B c= A & S1[B] implies S1[b2 \/ {b1}] )assume A6:
x in A
;
( B c= A & S1[B] implies S1[b2 \/ {b1}] )then reconsider fx =
F . x as
continuous Function of
X,
R by A3;
assume A7:
B c= A
;
( S1[B] implies S1[b2 \/ {b1}] )assume A8:
S1[
B]
;
S1[b2 \/ {b1}]per cases
( B = {} or B <> {} )
;
suppose A12:
B <> {}
;
S1[b2 \/ {b1}]then reconsider B9 =
B as non
empty set ;
consider f being
continuous Function of
X,
R such that A13:
for
x being
Point of
X for
S being non
empty finite Subset of
REAL st
S = rng ((commute (F | B9)) . x) holds
f . x = max S
by A8;
consider h being
continuous Function of
X,
R such that A14:
for
x being
Point of
X holds
h . x = max (
(f . x),
(fx . x))
by Th50;
thus
S1[
B \/ {x}]
verumproof
F is
Function of
A,
(Funcs ( the carrier of X, the carrier of R))
by A4, FUNCT_2:66;
then
F | B is
Function of
B,
(Funcs ( the carrier of X, the carrier of R))
by A7, FUNCT_2:32;
then
F | B in Funcs (
B,
(Funcs ( the carrier of X, the carrier of R)))
by FUNCT_2:8;
then
commute (F | B) in Funcs ( the
carrier of
X,
(Funcs (B, the carrier of R)))
by A12, FUNCT_6:55;
then reconsider cFB =
commute (F | B) as
Function of the
carrier of
X,
(Funcs (B, the carrier of R)) by FUNCT_2:66;
assume
not
B \/ {x} is
empty
;
ex f being continuous Function of X,R st
for x being Point of X
for S being non empty finite Subset of REAL st S = rng ((commute (F | (B \/ {x}))) . x) holds
f . x = max S
take
h
;
for x being Point of X
for S being non empty finite Subset of REAL st S = rng ((commute (F | (B \/ {x}))) . x) holds
h . x = max S
let a be
Point of
X;
for S being non empty finite Subset of REAL st S = rng ((commute (F | (B \/ {x}))) . a) holds
h . a = max Slet S be non
empty finite Subset of
REAL;
( S = rng ((commute (F | (B \/ {x}))) . a) implies h . a = max S )
reconsider cFBa =
cFB . a as
Function of
B9, the
carrier of
R ;
A15:
dom fx = the
carrier of
X
by FUNCT_2:def 1;
F | (B \/ {x}) = (F | B) \/ (F | {x})
by RELAT_1:78;
then A16:
(commute (F | (B \/ {x}))) . a = (cFB . a) \/ ((commute (F | {x})) . a)
by Th7;
assume
S = rng ((commute (F | (B \/ {x}))) . a)
;
h . a = max S
then A17:
S = (rng cFBa) \/ (rng ((commute (F | {x})) . a))
by A16, RELAT_1:12;
then
rng cFBa c= S
by XBOOLE_1:7;
then reconsider S1 =
rng cFBa as non
empty finite Subset of
REAL by XBOOLE_1:1;
F | {x} = x .--> (F . x)
by A2, A6, FUNCT_7:6;
then
(commute (F | {x})) . a = x .--> (fx . a)
by A15, Th3;
then A18:
S = S1 \/ {(fx . a)}
by A17, FUNCOP_1:8;
f . a = max S1
by A13;
then max S =
max (
(f . a),
(max {(fx . a)}))
by A18, XXREAL_2:10
.=
max (
(f . a),
(fx . a))
by XXREAL_2:11
;
hence
h . a = max S
by A14;
verum
end; end; end; end;
A19:
A is finite
;
S1[A]
from FINSET_1:sch 2(A19, A1, A5);
hence
ex f being continuous Function of X,R st
for x being Point of X
for S being non empty finite Subset of REAL st S = rng ((commute F) . x) holds
f . x = max S
; verum