let T be non empty TopSpace; :: thesis: for f being Function of T,R^1
for P being Subset of T st P <> {} & P is compact & f is continuous holds
ex x1, x2 being Point of T st
( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) )
let f be Function of T,R^1; :: thesis: for P being Subset of T st P <> {} & P is compact & f is continuous holds
ex x1, x2 being Point of T st
( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) )
let P be Subset of T; :: thesis: ( P <> {} & P is compact & f is continuous implies ex x1, x2 being Point of T st
( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) ) )
assume that
A1: P <> {} and
A2: ( P is compact & f is continuous ) ; :: thesis: ex x1, x2 being Point of T st
( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) )
A3: [#] (f .: P) <> {}
proof
consider x being object such that
A4: x in P by A1, XBOOLE_0:def 1;
dom f = the carrier of T by FUNCT_2:def 1;
then f . x in f .: P by A4, FUNCT_1:def 6;
hence [#] (f .: P) <> {} ; :: thesis: verum
end;
consider y1, y2 being Real such that
A5: y1 = upper_bound ([#] (f .: P)) and
A6: y2 = lower_bound ([#] (f .: P)) ;
A7: [#] (f .: P) is compact by A2, Th8, Th13;
then y1 in [#] (f .: P) by A3, A5, RCOMP_1:14;
then consider x1 being object such that
A8: x1 in dom f and
A9: ( x1 in P & y1 = f . x1 ) by FUNCT_1:def 6;
y2 in [#] (f .: P) by A3, A6, A7, RCOMP_1:14;
then consider x2 being object such that
A10: x2 in dom f and
A11: ( x2 in P & y2 = f . x2 ) by FUNCT_1:def 6;
reconsider x1 = x1, x2 = x2 as Point of T by A8, A10;
take x1 ; :: thesis: ex x2 being Point of T st
( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) )
take x2 ; :: thesis: ( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) )
thus ( x1 in P & x2 in P & f . x1 = upper_bound ([#] (f .: P)) & f . x2 = lower_bound ([#] (f .: P)) ) by A5, A6, A9, A11; :: thesis: verum