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 ext-real number ; 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:50;
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:116;
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:116;
assume Z:
not [.r,s.] c= f .: A
; contradiction
reconsider r = r, s = s as Real by A3, A6;
consider t being Real such that
A9:
t in [.r,s.]
and
A10:
not t in f .: A
by Z, SUBSET_1:7;
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);
A11:
f " (right_open_halfline t) is open
by PSCOMP_1:54;
t <= s
by A9, XXREAL_1:1;
then A12:
t < s
by A6, A10, 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 A12;
then
q in f " (right_open_halfline t)
by A8, FUNCT_2:46;
then A13:
(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
by XBOOLE_0:def 7;
then
f " (left_open_halfline t) misses f " (right_open_halfline t)
by FUNCT_1:141;
then
(f " (left_open_halfline t)) /\ (f " (right_open_halfline t)) = {}
by XBOOLE_0:def 7;
then A14:
(f " (left_open_halfline t)) /\ (f " (right_open_halfline t)) misses ((f " (left_open_halfline t)) /\ A) \/ ((f " (right_open_halfline t)) /\ A)
by XBOOLE_1:65;
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 A15: (f " Y) ` =
f " ((left_open_halfline t) \/ (right_open_halfline t))
by FUNCT_2:177
.=
(f " (left_open_halfline t)) \/ (f " (right_open_halfline t))
by RELAT_1:175
;
f " {t} misses f " (f .: A)
by A10, FUNCT_1:141, ZFMISC_1:56;
then
f " {t} misses A
by A2, XBOOLE_1:63;
then
A c= (f " (left_open_halfline t)) \/ (f " (right_open_halfline t))
by A15, SUBSET_1:43;
then A16: 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
;
A17:
(f " (left_open_halfline t)) /\ A c= f " (left_open_halfline t)
by XBOOLE_1:17;
r <= t
by A9, XXREAL_1:1;
then A18:
r < t
by A3, A10, 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 A18;
then
p in f " (left_open_halfline t)
by A5, FUNCT_2:46;
then A19:
(f " (left_open_halfline t)) /\ A <> {} T
by A4, XBOOLE_0:def 4;
A20:
(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:54;
then
(f " (left_open_halfline t)) /\ A,(f " (right_open_halfline t)) /\ A are_separated
by A11, A17, A20, A14, TSEP_1:49;
hence
contradiction
by A1, A16, A19, A13, CONNSP_1:16; verum