let n be Nat; :: thesis: 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 q being Point of (TOP-REAL n) ex G being Subset of REAL st

( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ) holds

lower_bound (f .: [:A,B:]) = lower_bound (g .: B)

let A, B be non empty compact Subset of (TOP-REAL n); :: thesis: for f being continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]

for g being RealMap of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) ex G being Subset of REAL st

( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ) holds

lower_bound (f .: [:A,B:]) = lower_bound (g .: B)

let f be continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]; :: thesis: for g being RealMap of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) ex G being Subset of REAL st

( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ) holds

lower_bound (f .: [:A,B:]) = lower_bound (g .: B)

let g be RealMap of (TOP-REAL n); :: thesis: ( ( for q being Point of (TOP-REAL n) ex G being Subset of REAL st

( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ) implies lower_bound (f .: [:A,B:]) = lower_bound (g .: B) )

assume A1: for q being Point of (TOP-REAL n) ex G being Subset of REAL st

( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ; :: thesis: lower_bound (f .: [:A,B:]) = lower_bound (g .: B)

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 .: B c= f .: [:A,B:]

A15: for r being Real st r in f .: [:A,B:] holds

lower_bound (g .: B) <= r

ex r being Real st

( r in f .: [:A,B:] & r < (lower_bound (g .: B)) + s )

for f being continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]

for g being RealMap of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) ex G being Subset of REAL st

( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ) holds

lower_bound (f .: [:A,B:]) = lower_bound (g .: B)

let A, B be non empty compact Subset of (TOP-REAL n); :: thesis: for f being continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]

for g being RealMap of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) ex G being Subset of REAL st

( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ) holds

lower_bound (f .: [:A,B:]) = lower_bound (g .: B)

let f be continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]; :: thesis: for g being RealMap of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) ex G being Subset of REAL st

( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ) holds

lower_bound (f .: [:A,B:]) = lower_bound (g .: B)

let g be RealMap of (TOP-REAL n); :: thesis: ( ( for q being Point of (TOP-REAL n) ex G being Subset of REAL st

( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ) implies lower_bound (f .: [:A,B:]) = lower_bound (g .: B) )

assume A1: for q being Point of (TOP-REAL n) ex G being Subset of REAL st

( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ; :: thesis: lower_bound (f .: [:A,B:]) = lower_bound (g .: B)

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 .: B c= f .: [:A,B:]

proof

then A14:
g .: B is bounded_below
by A4, XXREAL_2:44;
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in g .: B or u in f .: [:A,B:] )

assume u in g .: B ; :: thesis: u in f .: [:A,B:]

then consider q being Point of (TOP-REAL n) such that

A6: q in B and

A7: u = g . q by FUNCT_2:65;

consider p being Point of (TOP-REAL n) such that

A8: p in A by SUBSET_1:4;

consider G being Subset of REAL such that

A9: G = { (f . (p1,q)) where p1 is Point of (TOP-REAL n) : p1 in A } and

A10: u = lower_bound G by A1, A7;

A11: f . (p,q) in G by A8, A9;

G c= f .: [:A,B:]

end;assume u in g .: B ; :: thesis: u in f .: [:A,B:]

then consider q being Point of (TOP-REAL n) such that

A6: q in B and

A7: u = g . q by FUNCT_2:65;

consider p being Point of (TOP-REAL n) such that

A8: p in A by SUBSET_1:4;

consider G being Subset of REAL such that

A9: G = { (f . (p1,q)) where p1 is Point of (TOP-REAL n) : p1 in A } and

A10: u = lower_bound G by A1, A7;

A11: f . (p,q) in G by A8, A9;

G c= f .: [:A,B:]

proof

hence
u in f .: [:A,B:]
by A3, A10, A11, Th2; :: thesis: verum
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in G or u in f .: [:A,B:] )

assume u in G ; :: thesis: u in f .: [:A,B:]

then consider p1 being Point of (TOP-REAL n) such that

A12: u = f . (p1,q) and

A13: p1 in A by A9;

[p1,q] in [:A,B:] by A6, A13, ZFMISC_1:87;

hence u in f .: [:A,B:] by A12, FUNCT_2:35; :: thesis: verum

end;assume u in G ; :: thesis: u in f .: [:A,B:]

then consider p1 being Point of (TOP-REAL n) such that

A12: u = f . (p1,q) and

A13: p1 in A by A9;

[p1,q] in [:A,B:] by A6, A13, ZFMISC_1:87;

hence u in f .: [:A,B:] by A12, FUNCT_2:35; :: thesis: verum

A15: for r being Real st r in f .: [:A,B:] holds

lower_bound (g .: B) <= r

proof

for s being Real st 0 < s holds
let r be Real; :: thesis: ( r in f .: [:A,B:] implies lower_bound (g .: B) <= r )

assume r in f .: [:A,B:] ; :: thesis: lower_bound (g .: B) <= 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: p in A 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 . (p1,q)) where p1 is Point of (TOP-REAL n) : p1 in A } and

A23: g . q = lower_bound G by A1;

A24: q in B by A16, A20, ZFMISC_1:87;

G c= f .: [:A,B:]

r = f . (p,q) by A17, A20;

then r in G by A21, A22;

then A28: g . q <= r by A23, A27, SEQ_4:def 2;

g . q in g .: B by A24, FUNCT_2:35;

then lower_bound (g .: B) <= g . q by A14, SEQ_4:def 2;

hence lower_bound (g .: B) <= r by A28, XXREAL_0:2; :: thesis: verum

end;assume r in f .: [:A,B:] ; :: thesis: lower_bound (g .: B) <= 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: p in A 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 . (p1,q)) where p1 is Point of (TOP-REAL n) : p1 in A } and

A23: g . q = lower_bound G by A1;

A24: q in B by A16, A20, ZFMISC_1:87;

G c= f .: [:A,B:]

proof

then A27:
G is bounded_below
by A4, XXREAL_2:44;
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in G or u in f .: [:A,B:] )

assume u in G ; :: thesis: u in f .: [:A,B:]

then consider p1 being Point of (TOP-REAL n) such that

A25: u = f . (p1,q) and

A26: p1 in A by A22;

[p1,q] in [:A,B:] by A24, A26, ZFMISC_1:87;

hence u in f .: [:A,B:] by A25, FUNCT_2:35; :: thesis: verum

end;assume u in G ; :: thesis: u in f .: [:A,B:]

then consider p1 being Point of (TOP-REAL n) such that

A25: u = f . (p1,q) and

A26: p1 in A by A22;

[p1,q] in [:A,B:] by A24, A26, ZFMISC_1:87;

hence u in f .: [:A,B:] by A25, FUNCT_2:35; :: thesis: verum

r = f . (p,q) by A17, A20;

then r in G by A21, A22;

then A28: g . q <= r by A23, A27, SEQ_4:def 2;

g . q in g .: B by A24, FUNCT_2:35;

then lower_bound (g .: B) <= g . q by A14, SEQ_4:def 2;

hence lower_bound (g .: B) <= r by A28, XXREAL_0:2; :: thesis: verum

ex r being Real st

( r in f .: [:A,B:] & r < (lower_bound (g .: B)) + s )

proof

hence
lower_bound (f .: [:A,B:]) = lower_bound (g .: B)
by A4, A15, SEQ_4:def 2; :: thesis: verum
let s be Real; :: thesis: ( 0 < s implies ex r being Real st

( r in f .: [:A,B:] & r < (lower_bound (g .: B)) + s ) )

assume 0 < s ; :: thesis: ex r being Real st

( r in f .: [:A,B:] & r < (lower_bound (g .: B)) + s )

then consider r being Real such that

A29: r in g .: B and

A30: r < (lower_bound (g .: B)) + s by A14, SEQ_4:def 2;

take r ; :: thesis: ( r in f .: [:A,B:] & r < (lower_bound (g .: B)) + s )

thus r in f .: [:A,B:] by A5, A29; :: thesis: r < (lower_bound (g .: B)) + s

thus r < (lower_bound (g .: B)) + s by A30; :: thesis: verum

end;( r in f .: [:A,B:] & r < (lower_bound (g .: B)) + s ) )

assume 0 < s ; :: thesis: ex r being Real st

( r in f .: [:A,B:] & r < (lower_bound (g .: B)) + s )

then consider r being Real such that

A29: r in g .: B and

A30: r < (lower_bound (g .: B)) + s by A14, SEQ_4:def 2;

take r ; :: thesis: ( r in f .: [:A,B:] & r < (lower_bound (g .: B)) + s )

thus r in f .: [:A,B:] by A5, A29; :: thesis: r < (lower_bound (g .: B)) + s

thus r < (lower_bound (g .: B)) + s by A30; :: thesis: verum