:: The Brouwer Fixed Point Theorem for Intervals
:: by Toshihiko Watanabe
::
:: Received August 17, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users


begin

Lm1:  for a, b being real number
for x being set st x in [.a,b.] holds
x is Real
;

Lm2:  for a, b being real number
for x being Point of (Closed-Interval-TSpace (a,b)) st a <= b holds
x is Real
proofend;

theorem Th1: :: TREAL_1:1
for a, b being real number
for A being Subset of R^1 st A = [.a,b.] holds
A is closed
proofend;

theorem Th2: :: TREAL_1:2
for a, b being real number st a <= b holds
Closed-Interval-TSpace (a,b) is closed
proofend;

theorem :: TREAL_1:3
for a, c, d, b being real number st a <= c &amp; d <= b &amp; c <= d holds
Closed-Interval-TSpace (c,d) is closed SubSpace of Closed-Interval-TSpace (a,b)
proofend;

theorem :: TREAL_1:4
for a, c, b, d being real number st a <= c &amp; b <= d &amp; c <= b holds
( Closed-Interval-TSpace (a,d) = (Closed-Interval-TSpace (a,b)) union (Closed-Interval-TSpace (c,d)) &amp; Closed-Interval-TSpace (c,b) = (Closed-Interval-TSpace (a,b)) meet (Closed-Interval-TSpace (c,d)) )
proofend;

definition
let a, b be real number ;
assume A1: a <= b ;
func (#) (a,b) ->  Point of (Closed-Interval-TSpace (a,b)) equals :Def1: :: TREAL_1:def 1
a;
coherence
 a is Point of (Closed-Interval-TSpace (a,b))
proofend;
correctness
;
func(a,b) (#)  ->  Point of (Closed-Interval-TSpace (a,b)) equals :Def2: :: TREAL_1:def 2
b;
coherence
 b is Point of (Closed-Interval-TSpace (a,b))
proofend;
correctness
;
end;

:: deftheorem Def1 defines (#) TREAL_1:def_1_:_
 for a, b being real number st a <= b holds
(#) (a,b) = a;

:: deftheorem Def2 defines (#) TREAL_1:def_2_:_
 for a, b being real number st a <= b holds
(a,b) (#) = b;

theorem :: TREAL_1:5
( 0[01] = (#) (0,1) &amp; 1[01] = (0,1) (#) ) by Def1, Def2, BORSUK_1:def_14, BORSUK_1:def_15;

theorem :: TREAL_1:6
for a, b, c being real number st a <= b &amp; b <= c holds
( (#) (a,b) = (#) (a,c) &amp; (b,c) (#) = (a,c) (#) )
proofend;

begin

:: 2. Continuous Mappings Between Topological Intervals.
definition
let a, b be real number ;
assume B1: a <= b ;
let t1, t2 be Point of (Closed-Interval-TSpace (a,b));
func L[01] (t1,t2) ->  Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (a,b)) means :Def3: :: TREAL_1:def 3
 for s being Point of (Closed-Interval-TSpace (0,1)) holds it . s = ((1 - s) * t1) + (s * t2);
existence
 ex b1 being Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (a,b)) st
for s being Point of (Closed-Interval-TSpace (0,1)) holds b1 . s = ((1 - s) * t1) + (s * t2)
proofend;
uniqueness
 for b1, b2 being Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (a,b)) st ( for s being Point of (Closed-Interval-TSpace (0,1)) holds b1 . s = ((1 - s) * t1) + (s * t2) ) &amp; ( for s being Point of (Closed-Interval-TSpace (0,1)) holds b2 . s = ((1 - s) * t1) + (s * t2) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines L[01] TREAL_1:def_3_:_
 for a, b being real number st a <= b holds
for t1, t2 being Point of (Closed-Interval-TSpace (a,b))
for b5 being Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (a,b)) holds
( b5 = L[01] (t1,t2) iff for s being Point of (Closed-Interval-TSpace (0,1)) holds b5 . s = ((1 - s) * t1) + (s * t2) );

theorem Th7: :: TREAL_1:7
for a, b being real number st a <= b holds
for t1, t2 being Point of (Closed-Interval-TSpace (a,b))
for s being Point of (Closed-Interval-TSpace (0,1)) holds (L[01] (t1,t2)) . s = ((t2 - t1) * s) + t1
proofend;

theorem Th8: :: TREAL_1:8
for a, b being real number st a <= b holds
for t1, t2 being Point of (Closed-Interval-TSpace (a,b)) holds L[01] (t1,t2) is continuous
proofend;

theorem :: TREAL_1:9
for a, b being real number st a <= b holds
for t1, t2 being Point of (Closed-Interval-TSpace (a,b)) holds
( (L[01] (t1,t2)) . ((#) (0,1)) = t1 &amp; (L[01] (t1,t2)) . ((0,1) (#)) = t2 )
proofend;

theorem :: TREAL_1:10
L[01] (((#) (0,1)),((0,1) (#))) = id (Closed-Interval-TSpace (0,1))
proofend;

definition
let a, b be real number ;
assume B1: a < b ;
let t1, t2 be Point of (Closed-Interval-TSpace (0,1));
func P[01] (a,b,t1,t2) ->  Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (0,1)) means :Def4: :: TREAL_1:def 4
 for s being Point of (Closed-Interval-TSpace (a,b)) holds it . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a);
existence
 ex b1 being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (0,1)) st
for s being Point of (Closed-Interval-TSpace (a,b)) holds b1 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a)
proofend;
uniqueness
 for b1, b2 being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (0,1)) st ( for s being Point of (Closed-Interval-TSpace (a,b)) holds b1 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) ) &amp; ( for s being Point of (Closed-Interval-TSpace (a,b)) holds b2 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines P[01] TREAL_1:def_4_:_
 for a, b being real number st a < b holds
for t1, t2 being Point of (Closed-Interval-TSpace (0,1))
for b5 being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (0,1)) holds
( b5 = P[01] (a,b,t1,t2) iff for s being Point of (Closed-Interval-TSpace (a,b)) holds b5 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) );

theorem Th11: :: TREAL_1:11
for a, b being real number st a < b holds
for t1, t2 being Point of (Closed-Interval-TSpace (0,1))
for s being Point of (Closed-Interval-TSpace (a,b)) holds (P[01] (a,b,t1,t2)) . s = (((t2 - t1) / (b - a)) * s) + (((b * t1) - (a * t2)) / (b - a))
proofend;

theorem Th12: :: TREAL_1:12
for a, b being real number st a < b holds
for t1, t2 being Point of (Closed-Interval-TSpace (0,1)) holds P[01] (a,b,t1,t2) is continuous
proofend;

theorem :: TREAL_1:13
for a, b being real number st a < b holds
for t1, t2 being Point of (Closed-Interval-TSpace (0,1)) holds
( (P[01] (a,b,t1,t2)) . ((#) (a,b)) = t1 &amp; (P[01] (a,b,t1,t2)) . ((a,b) (#)) = t2 )
proofend;

theorem :: TREAL_1:14
P[01] (0,1,((#) (0,1)),((0,1) (#))) = id (Closed-Interval-TSpace (0,1))
proofend;

theorem Th15: :: TREAL_1:15
for a, b being real number st a < b holds
( id (Closed-Interval-TSpace (a,b)) = (L[01] (((#) (a,b)),((a,b) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#)))) &amp; id (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((#) (0,1)),((0,1) (#)))) * (L[01] (((#) (a,b)),((a,b) (#)))) )
proofend;

theorem Th16: :: TREAL_1:16
for a, b being real number st a < b holds
( id (Closed-Interval-TSpace (a,b)) = (L[01] (((a,b) (#)),((#) (a,b)))) * (P[01] (a,b,((0,1) (#)),((#) (0,1)))) &amp; id (Closed-Interval-TSpace (0,1)) = (P[01] (a,b,((0,1) (#)),((#) (0,1)))) * (L[01] (((a,b) (#)),((#) (a,b)))) )
proofend;

theorem Th17: :: TREAL_1:17
for a, b being real number st a < b holds
( L[01] (((#) (a,b)),((a,b) (#))) is being_homeomorphism &amp; (L[01] (((#) (a,b)),((a,b) (#)))) " = P[01] (a,b,((#) (0,1)),((0,1) (#))) &amp; P[01] (a,b,((#) (0,1)),((0,1) (#))) is being_homeomorphism &amp; (P[01] (a,b,((#) (0,1)),((0,1) (#)))) " = L[01] (((#) (a,b)),((a,b) (#))) )
proofend;

theorem :: TREAL_1:18
for a, b being real number st a < b holds
( L[01] (((a,b) (#)),((#) (a,b))) is being_homeomorphism &amp; (L[01] (((a,b) (#)),((#) (a,b)))) " = P[01] (a,b,((0,1) (#)),((#) (0,1))) &amp; P[01] (a,b,((0,1) (#)),((#) (0,1))) is being_homeomorphism &amp; (P[01] (a,b,((0,1) (#)),((#) (0,1)))) " = L[01] (((a,b) (#)),((#) (a,b))) )
proofend;

begin

:: 3. Connectedness of Intervals and Brouwer Fixed Point Theorem for Intervals.
theorem Th19: :: TREAL_1:19
I[01] is connected
proofend;

theorem :: TREAL_1:20
for a, b being real number st a <= b holds
Closed-Interval-TSpace (a,b) is connected
proofend;

theorem Th21: :: TREAL_1:21
for f being continuous Function of I[01],I[01] ex x being Point of I[01] st f . x = x
proofend;

theorem Th22: :: TREAL_1:22
for a, b being real number st a <= b holds
for f being continuous Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (a,b)) ex x being Point of (Closed-Interval-TSpace (a,b)) st f . x = x
proofend;

theorem Th23: :: TREAL_1:23
for X, Y being non empty SubSpace of R^1
for f being continuous Function of X,Y st ex a, b being Real st
( a <= b &amp; [.a,b.] c= the carrier of X &amp; [.a,b.] c= the carrier of Y &amp; f .: [.a,b.] c= [.a,b.] ) holds
ex x being Point of X st f . x = x
proofend;

:: [WP: ] Brouwer_Fixed_Point_Theorem_for_Intervals
theorem :: TREAL_1:24
for X, Y being non empty SubSpace of R^1
for f being continuous Function of X,Y st ex a, b being Real st
( a <= b &amp; [.a,b.] c= the carrier of X &amp; f .: [.a,b.] c= [.a,b.] ) holds
ex x being Point of X st f . x = x
proofend;