let T be non empty TopSpace; for f being continuous RealMap of T
for A being Subset of T st A is connected holds
f .: A is interval
let f be continuous RealMap of T; for A being Subset of T st A is connected holds
f .: A is interval
let A be Subset of T; ( A is connected implies f .: A is interval )
assume A1:
A is connected
; f .: A is interval
let r, s be ExtReal; XXREAL_2:def 12 ( not r in f .: A or not s in f .: A or [.r,s.] c= f .: A )
A2:
A c= f " (f .: A)
by FUNCT_2:42;
assume A3:
r in f .: A
; ( not s in f .: A or [.r,s.] c= f .: A )
then consider p being Point of T such that
A4:
p in A
and
A5:
r = f . p
by FUNCT_2:65;
assume A6:
s in f .: A
; [.r,s.] c= f .: A
then consider q being Point of T such that
A7:
q in A
and
A8:
s = f . q
by FUNCT_2:65;
assume A9:
not [.r,s.] c= f .: A
; contradiction
reconsider r = r, s = s as Real by A3, A6;
consider t being Element of REAL such that
A10:
t in [.r,s.]
and
A11:
not t in f .: A
by A9;
reconsider r = r, s = s, t = t as Real ;
set P1 = f " (left_open_halfline t);
set Q1 = f " (right_open_halfline t);
set P = (f " (left_open_halfline t)) /\ A;
set Q = (f " (right_open_halfline t)) /\ A;
set X = (left_open_halfline t) \/ (right_open_halfline t);
A12:
f " (right_open_halfline t) is open
by PSCOMP_1:8;
t <= s
by A10, XXREAL_1:1;
then A13:
t < s
by A6, A11, XXREAL_0:1;
right_open_halfline t = { r1 where r1 is Real : t < r1 }
by XXREAL_1:230;
then
s in right_open_halfline t
by A13;
then
q in f " (right_open_halfline t)
by A8, FUNCT_2:38;
then A14:
(f " (right_open_halfline t)) /\ A <> {} T
by A7, XBOOLE_0:def 4;
(left_open_halfline t) /\ (right_open_halfline t) =
].t,t.[
by XXREAL_1:269
.=
{}
by XXREAL_1:28
;
then
left_open_halfline t misses right_open_halfline t
;
then
f " (left_open_halfline t) misses f " (right_open_halfline t)
by FUNCT_1:71;
then
(f " (left_open_halfline t)) /\ (f " (right_open_halfline t)) = {}
;
then A15:
(f " (left_open_halfline t)) /\ (f " (right_open_halfline t)) misses ((f " (left_open_halfline t)) /\ A) \/ ((f " (right_open_halfline t)) /\ A)
;
reconsider Y = {t} as Subset of REAL ;
Y ` =
REAL \ [.t,t.]
by XXREAL_1:17
.=
(left_open_halfline t) \/ (right_open_halfline t)
by XXREAL_1:385
;
then A16: (f " Y) ` =
f " ((left_open_halfline t) \/ (right_open_halfline t))
by FUNCT_2:100
.=
(f " (left_open_halfline t)) \/ (f " (right_open_halfline t))
by RELAT_1:140
;
f " {t} misses f " (f .: A)
by A11, FUNCT_1:71, ZFMISC_1:50;
then
f " {t} misses A
by A2, XBOOLE_1:63;
then
A c= (f " (left_open_halfline t)) \/ (f " (right_open_halfline t))
by A16, SUBSET_1:23;
then A17: A =
A /\ ((f " (left_open_halfline t)) \/ (f " (right_open_halfline t)))
by XBOOLE_1:28
.=
((f " (left_open_halfline t)) /\ A) \/ ((f " (right_open_halfline t)) /\ A)
by XBOOLE_1:23
;
A18:
(f " (left_open_halfline t)) /\ A c= f " (left_open_halfline t)
by XBOOLE_1:17;
r <= t
by A10, XXREAL_1:1;
then A19:
r < t
by A3, A11, XXREAL_0:1;
left_open_halfline t = { r1 where r1 is Real : r1 < t }
by XXREAL_1:229;
then
r in left_open_halfline t
by A19;
then
p in f " (left_open_halfline t)
by A5, FUNCT_2:38;
then A20:
(f " (left_open_halfline t)) /\ A <> {} T
by A4, XBOOLE_0:def 4;
A21:
(f " (right_open_halfline t)) /\ A c= f " (right_open_halfline t)
by XBOOLE_1:17;
f " (left_open_halfline t) is open
by PSCOMP_1:8;
then
(f " (left_open_halfline t)) /\ A,(f " (right_open_halfline t)) /\ A are_separated
by A12, A18, A21, A15, TSEP_1:45;
hence
contradiction
by A1, A17, A20, A14, CONNSP_1:15; verum