let T be non empty TopSpace; :: thesis: ( ( for f being RealMap of T st f is continuous holds
f is bounded ) iff for f being RealMap of T st f is continuous holds
f is with_max )
set cT = the carrier of T;
hereby :: thesis: ( ( for f being RealMap of T st f is continuous holds
f is with_max ) implies for f being RealMap of T st f is continuous holds
f is bounded )
assume A1: for f being RealMap of T st f is continuous holds
f is bounded ; :: thesis: for f being RealMap of T st f is continuous holds
f is with_max
let f be RealMap of T; :: thesis: ( f is continuous implies f is with_max )
assume A2: f is continuous ; :: thesis: f is with_max
set fcT = f .: the carrier of T;
f is bounded by A1, A2;
then A3: f .: the carrier of T is bounded_above by MEASURE6:def 11;
set b = upper_bound (f .: the carrier of T);
set bf = (upper_bound (f .: the carrier of T)) + (- f);
- f is continuous by A2, Th9;
then A4: (upper_bound (f .: the carrier of T)) + (- f) is continuous by Th10;
reconsider bf9 = (upper_bound (f .: the carrier of T)) + (- f) as Function of the carrier of T,REAL ;
reconsider f9 = f as Function of the carrier of T,REAL ;
set g = Inv ((upper_bound (f .: the carrier of T)) + (- f));
set gcT = (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T;
assume not f is with_max ; :: thesis: contradiction
then A5: not f .: the carrier of T is with_max ;
then A6: not upper_bound (f .: the carrier of T) in f .: the carrier of T by A3;
now :: thesis: not 0 in rng ((upper_bound (f .: the carrier of T)) + (- f))
assume 0 in rng ((upper_bound (f .: the carrier of T)) + (- f)) ; :: thesis: contradiction
then consider x being object such that
A7: x in dom ((upper_bound (f .: the carrier of T)) + (- f)) and
A8: ((upper_bound (f .: the carrier of T)) + (- f)) . x = 0 by FUNCT_1:def 3;
reconsider x = x as Element of the carrier of T by A7;
bf9 . x = (upper_bound (f .: the carrier of T)) + ((- f9) . x) by VALUED_1:2
.= (upper_bound (f .: the carrier of T)) + (- (f . x)) by VALUED_1:8
.= (upper_bound (f .: the carrier of T)) - (f . x) ;
hence contradiction by A6, A8, FUNCT_2:35; :: thesis: verum
end;
then A9: Inv ((upper_bound (f .: the carrier of T)) + (- f)) is continuous by A4, Th11;
now :: thesis: ex a19 being Real st
( a19 > 0 & ( for r being Real st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= a19 ) )
Inv ((upper_bound (f .: the carrier of T)) + (- f)) is bounded by A1, A9;
then (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T is bounded_above by MEASURE6:def 11;
then consider p being Real such that
A10: p is UpperBound of (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T ;
A11: for r being Real st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= p by A10, XXREAL_2:def 1;
per cases ( p <= 0 or p > 0 ) ;
suppose A12: p <= 0 ; :: thesis: ex a19 being Real st
( a19 > 0 & ( for r being Real st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= a19 ) )
reconsider a19 = 1 as Real ;
take a19 = a19; :: thesis: ( a19 > 0 & ( for r being Real st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= a19 ) )
thus a19 > 0 ; :: thesis: for r being Real st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= a19
let r be Real; :: thesis: ( r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T implies r <= a19 )
assume r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T ; :: thesis: r <= a19
hence r <= a19 by A11, A12; :: thesis: verum
end;
suppose A13: p > 0 ; :: thesis: ex p being Real st
( p > 0 & ( for r being Real st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= p ) )
take p = p; :: thesis: ( p > 0 & ( for r being Real st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= p ) )
thus p > 0 by A13; :: thesis: for r being Real st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= p
thus for r being Real st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= p by A11; :: thesis: verum
end;
end;
end;
then consider p being Real such that
A14: p > 0 and
A15: for r being Real st r in (Inv ((upper_bound (f .: the carrier of T)) + (- f))) .: the carrier of T holds
r <= p ;
consider r being Real such that
A16: r in f .: the carrier of T and
A17: (upper_bound (f .: the carrier of T)) - (1 / p) < r by A3, A14, SEQ_4:def 1;
consider x being object such that
A18: x in the carrier of T and
x in the carrier of T and
A19: r = f . x by A16, FUNCT_2:64;
reconsider x = x as Element of T by A18;
A20: f . x <= upper_bound (f .: the carrier of T) by A3, A16, A19, SEQ_4:def 1;
f . x <> upper_bound (f .: the carrier of T) by A3, A5, A16, A19;
then (f . x) + 0 < upper_bound (f .: the carrier of T) by A20, XXREAL_0:1;
then A21: (upper_bound (f .: the carrier of T)) - (f . x) > 0 by XREAL_1:20;
(Inv ((upper_bound (f .: the carrier of T)) + (- f))) . x = (bf9 . x) " by VALUED_1:10
.= ((upper_bound (f .: the carrier of T)) + ((- f9) . x)) " by VALUED_1:2
.= 1 / ((upper_bound (f .: the carrier of T)) + ((- f9) . x))
.= 1 / ((upper_bound (f .: the carrier of T)) + (- (f . x))) by VALUED_1:8
.= 1 / ((upper_bound (f .: the carrier of T)) - (f . x)) ;
then 1 / ((upper_bound (f .: the carrier of T)) - (f . x)) <= p by A15, FUNCT_2:35;
then 1 <= p * ((upper_bound (f .: the carrier of T)) - (f . x)) by A21, XREAL_1:81;
then 1 / p <= (upper_bound (f .: the carrier of T)) - (f . x) by A14, XREAL_1:79;
then (f . x) + (1 / p) <= upper_bound (f .: the carrier of T) by XREAL_1:19;
hence contradiction by A17, A19, XREAL_1:19; :: thesis: verum
end;
assume A22: for f being RealMap of T st f is continuous holds
f is with_max ; :: thesis: for f being RealMap of T st f is continuous holds
f is bounded
let f be RealMap of T; :: thesis: ( f is continuous implies f is bounded )
assume A23: f is continuous ; :: thesis: f is bounded
then f is with_max by A22;
then f .: the carrier of T is with_max ;
then f .: the carrier of T is bounded_above ;
hence f is V49() ; :: according to SEQ_2:def 8 :: thesis: f is bounded_below
f is with_min by A22, A23, Th14;
then f .: the carrier of T is with_min ;
then f .: the carrier of T is bounded_below ;
hence f is bounded_below ; :: thesis: verum