let n be Element of 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:27;
then A3:
f .: [:A,B:] is compact
by Th2;
A4:
f .: [:A,B:] is bounded
by A2, Th2, RCOMP_1:28;
A5:
g .: A c= f .: [:A,B:]
proof
let u be
set ;
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:116;
consider q being
Point of
(TOP-REAL n) such that A8:
q in B
by SUBSET_1:10;
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, Th3;
verum
end;
then A14:
g .: A is bounded_below
by A4, XXREAL_2:44;
A15:
for r being real number st r in f .: [:A,B:] holds
lower_bound (g .: A) <= r
proof
let r be
real number ;
( 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:116;
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 5;
then consider p,
q being
set 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:103;
A21:
q in B
by A16, A20, ZFMISC_1:106;
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:106;
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 5;
g . p in g .: A
by A24, FUNCT_2:43;
then
lower_bound (g .: A) <= g . p
by A14, SEQ_4:def 5;
hence
lower_bound (g .: A) <= r
by A28, XXREAL_0:2;
verum
end;
for s being real number st 0 < s holds
ex r being real number 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 5; verum