let f be continuous Function of I[01],I[01]; ex x being Point of I[01] st f . x = x
reconsider F = f as Function of [.0,1.],[.0,1.] by BORSUK_1:40;
set A = { a where a is Real : ( a in [.0,1.] & F . a in [.0,a.] ) } ;
set B = { b where b is Real : ( b in [.0,1.] & F . b in [.b,1.] ) } ;
{ a where a is Real : ( a in [.0,1.] & F . a in [.0,a.] ) } c= REAL
then reconsider A = { a where a is Real : ( a in [.0,1.] & F . a in [.0,a.] ) } as Subset of REAL ;
A1:
Closed-Interval-TSpace (0,1) = TopSpaceMetr (Closed-Interval-MSpace (0,1))
by TOPMETR:def 7;
A2:
A c= [.0,1.]
{ b where b is Real : ( b in [.0,1.] & F . b in [.b,1.] ) } c= REAL
then reconsider B = { b where b is Real : ( b in [.0,1.] & F . b in [.b,1.] ) } as Subset of REAL ;
A4:
the carrier of (Closed-Interval-MSpace (0,1)) = [.0,1.]
by TOPMETR:10;
0 in { w where w is Real : ( 0 <= w & w <= 1 ) }
;
then A5:
0 in [.0,1.]
by RCOMP_1:def 1;
A6:
[.0,1.] <> {}
by XXREAL_1:1;
then
[.0,1.] = dom F
by FUNCT_2:def 1;
then
F . 0 in rng F
by A5, FUNCT_1:def 3;
then A7:
0 in B
by A5;
A8:
[.0,1.] = { q where q is Real : ( 0 <= q & q <= 1 ) }
by RCOMP_1:def 1;
A9:
[.0,1.] c= A \/ B
1 in { w where w is Real : ( 0 <= w & w <= 1 ) }
;
then A17:
1 in [.0,1.]
by RCOMP_1:def 1;
A18:
B c= [.0,1.]
assume A20:
for x being Point of I[01] holds f . x <> x
; contradiction
A21:
A /\ B = {}
proof
set x = the
Element of
A /\ B;
assume A22:
A /\ B <> {}
;
contradiction
then
the
Element of
A /\ B in A
by XBOOLE_0:def 4;
then A23:
ex
z being
Real st
(
z = the
Element of
A /\ B &
z in [.0,1.] &
F . z in [.0,z.] )
;
reconsider x = the
Element of
A /\ B as
Real ;
x in B
by A22, XBOOLE_0:def 4;
then
ex
b0 being
Real st
(
b0 = x &
b0 in [.0,1.] &
F . b0 in [.b0,1.] )
;
then A24:
F . x in [.0,x.] /\ [.x,1.]
by A23, XBOOLE_0:def 4;
x in { q where q is Real : ( 0 <= q & q <= 1 ) }
by A23, RCOMP_1:def 1;
then
ex
u being
Real st
(
u = x &
0 <= u &
u <= 1 )
;
then
F . x in {x}
by A24, XXREAL_1:418;
then
F . x = x
by TARSKI:def 1;
hence
contradiction
by A20, A23, BORSUK_1:40;
verum
end;
then A25:
A misses B
by XBOOLE_0:def 7;
[.0,1.] = dom F
by A6, FUNCT_2:def 1;
then
F . 1 in rng F
by A17, FUNCT_1:def 3;
then A26:
1 in A
by A17;
ex P, Q being Subset of I[01] st
( [#] I[01] = P \/ Q & P <> {} I[01] & Q <> {} I[01] & P is closed & Q is closed & P misses Q )
proof
reconsider P =
A,
Q =
B as
Subset of
I[01] by A2, A18, BORSUK_1:40;
take
P
;
ex Q being Subset of I[01] st
( [#] I[01] = P \/ Q & P <> {} I[01] & Q <> {} I[01] & P is closed & Q is closed & P misses Q )
take
Q
;
( [#] I[01] = P \/ Q & P <> {} I[01] & Q <> {} I[01] & P is closed & Q is closed & P misses Q )
thus A27:
[#] I[01] = P \/ Q
by A9, BORSUK_1:40, XBOOLE_0:def 10;
( P <> {} I[01] & Q <> {} I[01] & P is closed & Q is closed & P misses Q )
thus
(
P <> {} I[01] &
Q <> {} I[01] )
by A26, A7;
( P is closed & Q is closed & P misses Q )
thus
P is
closed
( Q is closed & P misses Q )proof
set z = the
Element of
(Cl P) /\ Q;
assume
not
P is
closed
;
contradiction
then A28:
Cl P <> P
by PRE_TOPC:22;
A29:
(Cl P) /\ Q <> {}
then A31:
the
Element of
(Cl P) /\ Q in Cl P
by XBOOLE_0:def 4;
A32:
the
Element of
(Cl P) /\ Q in Q
by A29, XBOOLE_0:def 4;
reconsider z = the
Element of
(Cl P) /\ Q as
Point of
I[01] by A31;
reconsider t0 =
z as
Real ;
A33:
ex
c being
Real st
(
c = t0 &
c in [.0,1.] &
F . c in [.c,1.] )
by A32;
then reconsider s0 =
F . t0 as
Real ;
t0 <= s0
by A33, XXREAL_1:1;
then A34:
0 <= s0 - t0
by XREAL_1:48;
set r =
(s0 - t0) * (2 ");
reconsider m =
z,
n =
f . z as
Point of
(Closed-Interval-MSpace (0,1)) by BORSUK_1:40, TOPMETR:10;
reconsider W =
Ball (
n,
((s0 - t0) * (2 "))) as
Subset of
I[01] by BORSUK_1:40, TOPMETR:10;
A35:
(
W is
open &
f is_continuous_at z )
by A1, TMAP_1:50, TOPMETR:14, TOPMETR:20;
A36:
s0 - t0 <> 0
by A20;
then A37:
0 / 2
< (s0 - t0) / 2
by A34, XREAL_1:74;
then
f . z in W
by TBSP_1:11;
then consider V being
Subset of
I[01] such that A38:
(
V is
open &
z in V )
and A39:
f .: V c= W
by A35, TMAP_1:43;
consider s being
Real such that A40:
s > 0
and A41:
Ball (
m,
s)
c= V
by A1, A38, TOPMETR:15, TOPMETR:20;
reconsider s =
s as
Real ;
set r0 =
min (
s,
((s0 - t0) * (2 ")));
reconsider W0 =
Ball (
m,
(min (s,((s0 - t0) * (2 "))))) as
Subset of
I[01] by BORSUK_1:40, TOPMETR:10;
min (
s,
((s0 - t0) * (2 ")))
> 0
by A37, A40, XXREAL_0:15;
then A42:
z in W0
by TBSP_1:11;
set w = the
Element of
P /\ W0;
W0 is
open
by A1, TOPMETR:14, TOPMETR:20;
then
P meets W0
by A31, A42, PRE_TOPC:24;
then A43:
P /\ W0 <> {} I[01]
by XBOOLE_0:def 7;
then A44:
the
Element of
P /\ W0 in P
by XBOOLE_0:def 4;
A45:
the
Element of
P /\ W0 in W0
by A43, XBOOLE_0:def 4;
then reconsider w = the
Element of
P /\ W0 as
Point of
(Closed-Interval-MSpace (0,1)) ;
reconsider w1 =
w as
Point of
I[01] by A44;
reconsider d =
w1 as
Real ;
A46:
d in A
by A43, XBOOLE_0:def 4;
Ball (
m,
(min (s,((s0 - t0) * (2 ")))))
= { q where q is Element of (Closed-Interval-MSpace (0,1)) : dist (m,q) < min (s,((s0 - t0) * (2 "))) }
by METRIC_1:17;
then
(
min (
s,
((s0 - t0) * (2 ")))
<= (s0 - t0) * (2 ") & ex
p being
Element of
(Closed-Interval-MSpace (0,1)) st
(
p = w &
dist (
m,
p)
< min (
s,
((s0 - t0) * (2 "))) ) )
by A45, XXREAL_0:17;
then
dist (
w,
m)
< (s0 - t0) * (2 ")
by XXREAL_0:2;
then A47:
|.(d - t0).| < (s0 - t0) * (2 ")
by HEINE:1;
d - t0 <= |.(d - t0).|
by ABSVALUE:4;
then
(
t0 + ((s0 - t0) * (2 ")) = s0 - ((s0 - t0) * (2 ")) &
d - t0 < (s0 - t0) * (2 ") )
by A47, XXREAL_0:2;
then A48:
d < s0 - ((s0 - t0) * (2 "))
by XREAL_1:19;
A49:
(s0 - t0) * (2 ") < (s0 - t0) * 1
by A34, A36, XREAL_1:68;
A50:
Ball (
n,
((s0 - t0) * (2 ")))
c= [.t0,1.]
proof
let x be
object ;
TARSKI:def 3 ( not x in Ball (n,((s0 - t0) * (2 "))) or x in [.t0,1.] )
assume A51:
x in Ball (
n,
((s0 - t0) * (2 ")))
;
x in [.t0,1.]
then reconsider u =
x as
Point of
(Closed-Interval-MSpace (0,1)) ;
x in [.0,1.]
by A4, A51;
then reconsider t =
x as
Real ;
Ball (
n,
((s0 - t0) * (2 ")))
= { q where q is Element of (Closed-Interval-MSpace (0,1)) : dist (n,q) < (s0 - t0) * (2 ") }
by METRIC_1:17;
then
ex
p being
Element of
(Closed-Interval-MSpace (0,1)) st
(
p = u &
dist (
n,
p)
< (s0 - t0) * (2 ") )
by A51;
then
|.(s0 - t).| < (s0 - t0) * (2 ")
by HEINE:1;
then A52:
|.(s0 - t).| < s0 - t0
by A49, XXREAL_0:2;
s0 - t <= |.(s0 - t).|
by ABSVALUE:4;
then
s0 - t < s0 - t0
by A52, XXREAL_0:2;
then A53:
t0 <= t
by XREAL_1:10;
t <= 1
by A4, A51, XXREAL_1:1;
then
t in { q where q is Real : ( t0 <= q & q <= 1 ) }
by A53;
hence
x in [.t0,1.]
by RCOMP_1:def 1;
verum
end;
A54:
Ball (
n,
((s0 - t0) * (2 ")))
c= [.d,1.]
proof
let x be
object ;
TARSKI:def 3 ( not x in Ball (n,((s0 - t0) * (2 "))) or x in [.d,1.] )
assume A55:
x in Ball (
n,
((s0 - t0) * (2 ")))
;
x in [.d,1.]
then reconsider v =
x as
Point of
(Closed-Interval-MSpace (0,1)) ;
x in [.0,1.]
by A4, A55;
then reconsider t =
x as
Real ;
Ball (
n,
((s0 - t0) * (2 ")))
= { q where q is Element of (Closed-Interval-MSpace (0,1)) : dist (n,q) < (s0 - t0) * (2 ") }
by METRIC_1:17;
then
ex
p being
Element of
(Closed-Interval-MSpace (0,1)) st
(
p = v &
dist (
n,
p)
< (s0 - t0) * (2 ") )
by A55;
then A56:
|.(s0 - t).| < (s0 - t0) * (2 ")
by HEINE:1;
t <= 1
by A50, A55, XXREAL_1:1;
then
t in { w0 where w0 is Real : ( d <= w0 & w0 <= 1 ) }
by A57;
hence
x in [.d,1.]
by RCOMP_1:def 1;
verum
end;
Ball (
m,
(min (s,((s0 - t0) * (2 ")))))
c= Ball (
m,
s)
by PCOMPS_1:1, XXREAL_0:17;
then
W0 c= V
by A41;
then
f . w1 in f .: V
by A45, FUNCT_2:35;
then
f . w1 in W
by A39;
then
d in B
by A54, BORSUK_1:40;
hence
contradiction
by A25, A46, XBOOLE_0:3;
verum
end;
thus
Q is
closed
P misses Qproof
set z = the
Element of
(Cl Q) /\ P;
assume
not
Q is
closed
;
contradiction
then A59:
Cl Q <> Q
by PRE_TOPC:22;
A60:
(Cl Q) /\ P <> {}
then A62:
the
Element of
(Cl Q) /\ P in Cl Q
by XBOOLE_0:def 4;
A63:
the
Element of
(Cl Q) /\ P in P
by A60, XBOOLE_0:def 4;
reconsider z = the
Element of
(Cl Q) /\ P as
Point of
I[01] by A62;
reconsider t0 =
z as
Real ;
A64:
ex
c being
Real st
(
c = t0 &
c in [.0,1.] &
F . c in [.0,c.] )
by A63;
then reconsider s0 =
F . t0 as
Real ;
s0 <= t0
by A64, XXREAL_1:1;
then A65:
0 <= t0 - s0
by XREAL_1:48;
set r =
(t0 - s0) * (2 ");
reconsider m =
z,
n =
f . z as
Point of
(Closed-Interval-MSpace (0,1)) by BORSUK_1:40, TOPMETR:10;
reconsider W =
Ball (
n,
((t0 - s0) * (2 "))) as
Subset of
I[01] by BORSUK_1:40, TOPMETR:10;
A66:
(
W is
open &
f is_continuous_at z )
by A1, TMAP_1:50, TOPMETR:14, TOPMETR:20;
A67:
t0 - s0 <> 0
by A20;
then A68:
0 / 2
< (t0 - s0) / 2
by A65, XREAL_1:74;
then
f . z in W
by TBSP_1:11;
then consider V being
Subset of
I[01] such that A69:
(
V is
open &
z in V )
and A70:
f .: V c= W
by A66, TMAP_1:43;
consider s being
Real such that A71:
s > 0
and A72:
Ball (
m,
s)
c= V
by A1, A69, TOPMETR:15, TOPMETR:20;
reconsider s =
s as
Real ;
set r0 =
min (
s,
((t0 - s0) * (2 ")));
reconsider W0 =
Ball (
m,
(min (s,((t0 - s0) * (2 "))))) as
Subset of
I[01] by BORSUK_1:40, TOPMETR:10;
min (
s,
((t0 - s0) * (2 ")))
> 0
by A68, A71, XXREAL_0:15;
then A73:
z in W0
by TBSP_1:11;
set w = the
Element of
Q /\ W0;
W0 is
open
by A1, TOPMETR:14, TOPMETR:20;
then
Q meets W0
by A62, A73, PRE_TOPC:24;
then A74:
Q /\ W0 <> {} I[01]
by XBOOLE_0:def 7;
then A75:
the
Element of
Q /\ W0 in Q
by XBOOLE_0:def 4;
A76:
the
Element of
Q /\ W0 in W0
by A74, XBOOLE_0:def 4;
then reconsider w = the
Element of
Q /\ W0 as
Point of
(Closed-Interval-MSpace (0,1)) ;
reconsider w1 =
w as
Point of
I[01] by A75;
reconsider d =
w1 as
Real ;
A77:
d in B
by A74, XBOOLE_0:def 4;
Ball (
m,
(min (s,((t0 - s0) * (2 ")))))
= { q where q is Element of (Closed-Interval-MSpace (0,1)) : dist (m,q) < min (s,((t0 - s0) * (2 "))) }
by METRIC_1:17;
then
(
min (
s,
((t0 - s0) * (2 ")))
<= (t0 - s0) * (2 ") & ex
p being
Element of
(Closed-Interval-MSpace (0,1)) st
(
p = w &
dist (
m,
p)
< min (
s,
((t0 - s0) * (2 "))) ) )
by A76, XXREAL_0:17;
then
dist (
m,
w)
< (t0 - s0) * (2 ")
by XXREAL_0:2;
then A78:
|.(t0 - d).| < (t0 - s0) * (2 ")
by HEINE:1;
t0 - d <= |.(t0 - d).|
by ABSVALUE:4;
then
t0 + (- d) < (t0 - s0) * (2 ")
by A78, XXREAL_0:2;
then
t0 < ((t0 - s0) * (2 ")) - (- d)
by XREAL_1:20;
then
(
s0 + ((t0 - s0) * (2 ")) = t0 - ((t0 - s0) * (2 ")) &
t0 < ((t0 - s0) * (2 ")) + (- (- d)) )
;
then A79:
s0 + ((t0 - s0) * (2 ")) < d
by XREAL_1:19;
A80:
(t0 - s0) * (2 ") < (t0 - s0) * 1
by A65, A67, XREAL_1:68;
A81:
Ball (
n,
((t0 - s0) * (2 ")))
c= [.0,t0.]
proof
let x be
object ;
TARSKI:def 3 ( not x in Ball (n,((t0 - s0) * (2 "))) or x in [.0,t0.] )
assume A82:
x in Ball (
n,
((t0 - s0) * (2 ")))
;
x in [.0,t0.]
then reconsider u =
x as
Point of
(Closed-Interval-MSpace (0,1)) ;
x in [.0,1.]
by A4, A82;
then reconsider t =
x as
Real ;
Ball (
n,
((t0 - s0) * (2 ")))
= { q where q is Element of (Closed-Interval-MSpace (0,1)) : dist (n,q) < (t0 - s0) * (2 ") }
by METRIC_1:17;
then
ex
p being
Element of
(Closed-Interval-MSpace (0,1)) st
(
p = u &
dist (
n,
p)
< (t0 - s0) * (2 ") )
by A82;
then
|.(t - s0).| < (t0 - s0) * (2 ")
by HEINE:1;
then A83:
|.(t - s0).| < t0 - s0
by A80, XXREAL_0:2;
t - s0 <= |.(t - s0).|
by ABSVALUE:4;
then
t - s0 < t0 - s0
by A83, XXREAL_0:2;
then A84:
t <= t0
by XREAL_1:9;
0 <= t
by A4, A82, XXREAL_1:1;
then
t in { q where q is Real : ( 0 <= q & q <= t0 ) }
by A84;
hence
x in [.0,t0.]
by RCOMP_1:def 1;
verum
end;
A85:
Ball (
n,
((t0 - s0) * (2 ")))
c= [.0,d.]
proof
let x be
object ;
TARSKI:def 3 ( not x in Ball (n,((t0 - s0) * (2 "))) or x in [.0,d.] )
assume A86:
x in Ball (
n,
((t0 - s0) * (2 ")))
;
x in [.0,d.]
then reconsider v =
x as
Point of
(Closed-Interval-MSpace (0,1)) ;
x in [.0,1.]
by A4, A86;
then reconsider t =
x as
Real ;
Ball (
n,
((t0 - s0) * (2 ")))
= { q where q is Element of (Closed-Interval-MSpace (0,1)) : dist (n,q) < (t0 - s0) * (2 ") }
by METRIC_1:17;
then
ex
p being
Element of
(Closed-Interval-MSpace (0,1)) st
(
p = v &
dist (
n,
p)
< (t0 - s0) * (2 ") )
by A86;
then A87:
|.(t - s0).| < (t0 - s0) * (2 ")
by HEINE:1;
0 <= t
by A81, A86, XXREAL_1:1;
then
t in { w0 where w0 is Real : ( 0 <= w0 & w0 <= d ) }
by A88;
hence
x in [.0,d.]
by RCOMP_1:def 1;
verum
end;
Ball (
m,
(min (s,((t0 - s0) * (2 ")))))
c= Ball (
m,
s)
by PCOMPS_1:1, XXREAL_0:17;
then
W0 c= V
by A72;
then
f . w1 in f .: V
by A76, FUNCT_2:35;
then
f . w1 in W
by A70;
then
d in A
by A85, BORSUK_1:40;
hence
contradiction
by A25, A77, XBOOLE_0:3;
verum
end;
thus
P misses Q
by A21, XBOOLE_0:def 7;
verum
end;
hence
contradiction
by Th19, CONNSP_1:10; verum