let T be non empty TopSpace; ( T is compact implies T is pseudocompact )
assume A1:
T is compact
; T is pseudocompact
let f be RealMap of T; PSCOMP_1:def 4 ( f is continuous implies f is bounded )
assume A2:
f is continuous
; f is bounded
thus
f is bounded_above
SEQ_2:def 8 f is bounded_below proof
set p = the
Element of
T;
defpred S1[
Real]
means c1 >= f . the
Element of
T;
set R =
{ (right_closed_halfline r3) where r3 is Element of REAL : S1[r3] } ;
A3:
{ (right_closed_halfline r3) where r3 is Element of REAL : S1[r3] } is
Subset-Family of
REAL
from DOMAIN_1:sch 8();
A4:
right_closed_halfline (f . the Element of T) in { (right_closed_halfline r3) where r3 is Element of REAL : S1[r3] }
;
then reconsider R =
{ (right_closed_halfline r3) where r3 is Element of REAL : S1[r3] } as non
empty Subset-Family of
REAL by A3;
reconsider F =
(" f) .: R as
Subset-Family of
T ;
A5:
F is
c=-linear
proof
let X,
Y be
set ;
ORDINAL1:def 8 ( not X in F or not Y in F or X,Y are_c=-comparable )
assume
X in F
;
( not Y in F or X,Y are_c=-comparable )
then consider A being
object such that A6:
A in bool REAL
and A7:
A in R
and A8:
X = (" f) . A
by FUNCT_2:64;
reconsider A =
A as
set by TARSKI:1;
A9:
X = f " A
by A6, A8, MEASURE6:def 3;
consider r1 being
Element of
REAL such that A10:
A = right_closed_halfline r1
and
r1 >= f . the
Element of
T
by A7;
assume
Y in F
;
X,Y are_c=-comparable
then consider B being
object such that A11:
B in bool REAL
and A12:
B in R
and A13:
Y = (" f) . B
by FUNCT_2:64;
reconsider B =
B as
set by TARSKI:1;
A14:
Y = f " B
by A11, A13, MEASURE6:def 3;
consider r2 being
Element of
REAL such that A15:
B = right_closed_halfline r2
and
r2 >= f . the
Element of
T
by A12;
(
r1 >= r2 or
r2 >= r1 )
;
then
(
X c= Y or
Y c= X )
by A10, A15, A9, A14, RELAT_1:143, XXREAL_1:38;
hence
X,
Y are_c=-comparable
by XBOOLE_0:def 9;
verum
end;
assume A16:
for
s being
Real holds
s is not
UpperBound of
f .: the
carrier of
T
;
XXREAL_2:def 10,
MEASURE6:def 11 contradiction
then A25:
F is
with_non-empty_elements
by SETFAM_1:def 8;
R is
closed
then A26:
F is
closed
by A2, Th13;
(" f) . (right_closed_halfline (f . the Element of T)) in F
by A4, FUNCT_2:35;
then
meet F <> {}
by A1, A25, A5, A26, COMPTS_1:4;
then consider x being
object such that A27:
x in meet F
by XBOOLE_0:def 1;
set eR = the
Element of
R;
the
Element of
R in R
;
then consider er being
Element of
REAL such that A28:
the
Element of
R = right_closed_halfline er
and A29:
er >= f . the
Element of
T
;
reconsider x =
x as
Element of
T by A27;
A30:
f . x in meet R
by A27, MEASURE6:35;
then A31:
f . x in the
Element of
R
by SETFAM_1:def 1;
consider fx9 being
Real such that A32:
fx9 > f . x
by XREAL_1:1;
reconsider fx9 =
fx9 as
Element of
REAL by XREAL_0:def 1;
right_closed_halfline er = { r3 where r3 is Real : r3 >= er }
by XXREAL_1:232;
then
ex
r1 being
Real st
(
f . x = r1 &
r1 >= er )
by A31, A28;
then
f . x >= f . the
Element of
T
by A29, XXREAL_0:2;
then
fx9 >= f . the
Element of
T
by A32, XXREAL_0:2;
then
right_closed_halfline fx9 in R
;
then A33:
f . x in right_closed_halfline fx9
by A30, SETFAM_1:def 1;
right_closed_halfline fx9 = { r3 where r3 is Real : r3 >= fx9 }
by XXREAL_1:232;
then
ex
r3 being
Real st
(
f . x = r3 &
r3 >= fx9 )
by A33;
hence
contradiction
by A32;
verum
end;
set p = the Element of T;
defpred S1[ Real] means c1 <= f . the Element of T;
set R = { (left_closed_halfline r3) where r3 is Element of REAL : S1[r3] } ;
A34:
{ (left_closed_halfline r3) where r3 is Element of REAL : S1[r3] } is Subset-Family of REAL
from DOMAIN_1:sch 8();
A35:
left_closed_halfline (f . the Element of T) in { (left_closed_halfline r3) where r3 is Element of REAL : S1[r3] }
;
then reconsider R = { (left_closed_halfline r3) where r3 is Element of REAL : S1[r3] } as non empty Subset-Family of REAL by A34;
reconsider F = (" f) .: R as Subset-Family of T ;
R is closed
then A36:
F is closed
by A2, Th13;
A37:
F is c=-linear
proof
let X,
Y be
set ;
ORDINAL1:def 8 ( not X in F or not Y in F or X,Y are_c=-comparable )
assume
X in F
;
( not Y in F or X,Y are_c=-comparable )
then consider A being
object such that A38:
A in bool REAL
and A39:
A in R
and A40:
X = (" f) . A
by FUNCT_2:64;
reconsider A =
A as
set by TARSKI:1;
A41:
X = f " A
by A38, A40, MEASURE6:def 3;
consider r1 being
Element of
REAL such that A42:
A = left_closed_halfline r1
and
r1 <= f . the
Element of
T
by A39;
assume
Y in F
;
X,Y are_c=-comparable
then consider B being
object such that A43:
B in bool REAL
and A44:
B in R
and A45:
Y = (" f) . B
by FUNCT_2:64;
reconsider B =
B as
set by TARSKI:1;
A46:
Y = f " B
by A43, A45, MEASURE6:def 3;
consider r2 being
Element of
REAL such that A47:
B = left_closed_halfline r2
and
r2 <= f . the
Element of
T
by A44;
(
r1 <= r2 or
r2 <= r1 )
;
then
(
X c= Y or
Y c= X )
by A42, A47, A41, A46, RELAT_1:143, XXREAL_1:42;
hence
X,
Y are_c=-comparable
by XBOOLE_0:def 9;
verum
end;
assume A48:
for s being Real holds s is not LowerBound of f .: the carrier of T
; XXREAL_2:def 9,MEASURE6:def 10 contradiction
then A57:
F is with_non-empty_elements
by SETFAM_1:def 8;
(" f) . (left_closed_halfline (f . the Element of T)) in F
by A35, FUNCT_2:35;
then
meet F <> {}
by A1, A57, A37, A36, COMPTS_1:4;
then consider x being object such that
A58:
x in meet F
by XBOOLE_0:def 1;
set eR = the Element of R;
the Element of R in R
;
then consider er being Element of REAL such that
A59:
the Element of R = left_closed_halfline er
and
A60:
er <= f . the Element of T
;
reconsider x = x as Element of T by A58;
A61:
f . x in meet R
by A58, MEASURE6:35;
then A62:
f . x in the Element of R
by SETFAM_1:def 1;
consider fx9 being Real such that
A63:
fx9 < f . x
by XREAL_1:2;
reconsider fx9 = fx9 as Element of REAL by XREAL_0:def 1;
left_closed_halfline er = { r3 where r3 is Real : r3 <= er }
by XXREAL_1:231;
then
ex r1 being Real st
( f . x = r1 & r1 <= er )
by A62, A59;
then
f . x <= f . the Element of T
by A60, XXREAL_0:2;
then
fx9 <= f . the Element of T
by A63, XXREAL_0:2;
then
left_closed_halfline fx9 in R
;
then A64:
f . x in left_closed_halfline fx9
by A61, SETFAM_1:def 1;
left_closed_halfline fx9 = { r3 where r3 is Real : r3 <= fx9 }
by XXREAL_1:231;
then
ex r3 being Real st
( f . x = r3 & r3 <= fx9 )
by A64;
hence
contradiction
by A63; verum