let n be Nat; for A, B being non empty compact Subset of (TOP-REAL n)
for f being continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]
for g being RealMap of (TOP-REAL n) st ( for p being Point of (TOP-REAL n) ex G being Subset of REAL st
( G = { (f . (p,q)) where q is Point of (TOP-REAL n) : q in B } & g . p = lower_bound G ) ) holds
lower_bound (f .: [:A,B:]) = lower_bound (g .: A)
let A, B be non empty compact Subset of (TOP-REAL n); for f being continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]
for g being RealMap of (TOP-REAL n) st ( for p being Point of (TOP-REAL n) ex G being Subset of REAL st
( G = { (f . (p,q)) where q is Point of (TOP-REAL n) : q in B } & g . p = lower_bound G ) ) holds
lower_bound (f .: [:A,B:]) = lower_bound (g .: A)
let f be continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]; for g being RealMap of (TOP-REAL n) st ( for p being Point of (TOP-REAL n) ex G being Subset of REAL st
( G = { (f . (p,q)) where q is Point of (TOP-REAL n) : q in B } & g . p = lower_bound G ) ) holds
lower_bound (f .: [:A,B:]) = lower_bound (g .: A)
let g be RealMap of (TOP-REAL n); ( ( for p being Point of (TOP-REAL n) ex G being Subset of REAL st
( G = { (f . (p,q)) where q is Point of (TOP-REAL n) : q in B } & g . p = lower_bound G ) ) implies lower_bound (f .: [:A,B:]) = lower_bound (g .: A) )
assume A1:
for p being Point of (TOP-REAL n) ex G being Subset of REAL st
( G = { (f . (p,q)) where q is Point of (TOP-REAL n) : q in B } & g . p = lower_bound G )
; lower_bound (f .: [:A,B:]) = lower_bound (g .: A)
A2:
[:A,B:] is compact
by BORSUK_3:23;
then A3:
f .: [:A,B:] is compact
by Th1;
A4:
f .: [:A,B:] is real-bounded
by A2, Th1, RCOMP_1:10;
A5:
g .: A c= f .: [:A,B:]
proof
let u be
object ;
TARSKI:def 3 ( not u in g .: A or u in f .: [:A,B:] )
assume
u in g .: A
;
u in f .: [:A,B:]
then consider p being
Point of
(TOP-REAL n) such that A6:
p in A
and A7:
u = g . p
by FUNCT_2:65;
consider q being
Point of
(TOP-REAL n) such that A8:
q in B
by SUBSET_1:4;
consider G being
Subset of
REAL such that A9:
G = { (f . (p,q1)) where q1 is Point of (TOP-REAL n) : q1 in B }
and A10:
u = lower_bound G
by A1, A7;
A11:
f . (
p,
q)
in G
by A8, A9;
G c= f .: [:A,B:]
hence
u in f .: [:A,B:]
by A3, A10, A11, Th2;
verum
end;
then A14:
g .: A is bounded_below
by A4, XXREAL_2:44;
A15:
for r being Real st r in f .: [:A,B:] holds
lower_bound (g .: A) <= r
proof
let r be
Real;
( r in f .: [:A,B:] implies lower_bound (g .: A) <= r )
assume
r in f .: [:A,B:]
;
lower_bound (g .: A) <= r
then consider pq being
Point of
[:(TOP-REAL n),(TOP-REAL n):] such that A16:
pq in [:A,B:]
and A17:
r = f . pq
by FUNCT_2:65;
pq in the
carrier of
[:(TOP-REAL n),(TOP-REAL n):]
;
then
pq in [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):]
by BORSUK_1:def 2;
then consider p,
q being
object such that A18:
p in the
carrier of
(TOP-REAL n)
and A19:
q in the
carrier of
(TOP-REAL n)
and A20:
pq = [p,q]
by ZFMISC_1:84;
A21:
q in B
by A16, A20, ZFMISC_1:87;
reconsider p =
p,
q =
q as
Point of
(TOP-REAL n) by A18, A19;
consider G being
Subset of
REAL such that A22:
G = { (f . (p,q1)) where q1 is Point of (TOP-REAL n) : q1 in B }
and A23:
g . p = lower_bound G
by A1;
A24:
p in A
by A16, A20, ZFMISC_1:87;
G c= f .: [:A,B:]
then A27:
G is
bounded_below
by A4, XXREAL_2:44;
r = f . (
p,
q)
by A17, A20;
then
r in G
by A21, A22;
then A28:
g . p <= r
by A23, A27, SEQ_4:def 2;
g . p in g .: A
by A24, FUNCT_2:35;
then
lower_bound (g .: A) <= g . p
by A14, SEQ_4:def 2;
hence
lower_bound (g .: A) <= r
by A28, XXREAL_0:2;
verum
end;
for s being Real st 0 < s holds
ex r being Real st
( r in f .: [:A,B:] & r < (lower_bound (g .: A)) + s )
hence
lower_bound (f .: [:A,B:]) = lower_bound (g .: A)
by A4, A15, SEQ_4:def 2; verum