:: The Brouwer Fixed Point Theorem for Intervals
:: by Toshihiko Watanabe
::
:: Copyright (c) 1992 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 () st a <= b holds
x is Real
proof end;

theorem :: TREAL_1:1
canceled;

theorem :: TREAL_1:2
canceled;

theorem :: TREAL_1:3
canceled;

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

theorem Th5: :: TREAL_1:5
for a, b being real number st a <= b holds
Closed-Interval-TSpace (a,b) is closed
proof end;

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

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

definition
let a, b be real number ;
assume A1: a <= b ;
func (#) (a,b) -> Point of () equals :Def1: :: TREAL_1:def 1
a;
coherence
a is Point of ()
proof end;
correctness
;
func (a,b) (#) -> Point of () equals :Def2: :: TREAL_1:def 2
b;
coherence
b is Point of ()
proof end;
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:8
( 0 = (#) (0,1) & 1 = (0,1) (#) ) by ;

theorem :: TREAL_1:9
for a, b, c being real number st a <= b & b <= c holds
( (#) (a,b) = (#) (a,c) & (b,c) (#) = (a,c) (#) )
proof end;

begin

definition
let a, b be real number ;
assume A1: a <= b ;
let t1, t2 be Point of ();
func L (t1,t2) -> Function of (),() means :Def3: :: TREAL_1:def 3
for s being Point of () holds it . s = ((1 - s) * t1) + (s * t2);
existence
ex b1 being Function of (),() st
for s being Point of () holds b1 . s = ((1 - s) * t1) + (s * t2)
proof end;
uniqueness
for b1, b2 being Function of (),() st ( for s being Point of () holds b1 . s = ((1 - s) * t1) + (s * t2) ) & ( for s being Point of () holds b2 . s = ((1 - s) * t1) + (s * t2) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines L TREAL_1:def 3 :
for a, b being real number st a <= b holds
for t1, t2 being Point of ()
for b5 being Function of (),() holds
( b5 = L (t1,t2) iff for s being Point of () holds b5 . s = ((1 - s) * t1) + (s * t2) );

theorem Th10: :: TREAL_1:10
for a, b being real number st a <= b holds
for t1, t2 being Point of ()
for s being Point of () holds (L (t1,t2)) . s = ((t2 - t1) * s) + t1
proof end;

theorem Th11: :: TREAL_1:11
for a, b being real number st a <= b holds
for t1, t2 being Point of () holds L (t1,t2) is continuous
proof end;

theorem :: TREAL_1:12
for a, b being real number st a <= b holds
for t1, t2 being Point of () holds
( (L (t1,t2)) . ((#) (0,1)) = t1 & (L (t1,t2)) . ((0,1) (#)) = t2 )
proof end;

theorem :: TREAL_1:13
L (((#) (0,1)),((0,1) (#))) = id ()
proof end;

definition
let a, b be real number ;
assume A1: a < b ;
let t1, t2 be Point of ();
func P (a,b,t1,t2) -> Function of (),() means :Def4: :: TREAL_1:def 4
for s being Point of () holds it . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a);
existence
ex b1 being Function of (),() st
for s being Point of () holds b1 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a)
proof end;
uniqueness
for b1, b2 being Function of (),() st ( for s being Point of () holds b1 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) ) & ( for s being Point of () holds b2 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines P TREAL_1:def 4 :
for a, b being real number st a < b holds
for t1, t2 being Point of ()
for b5 being Function of (),() holds
( b5 = P (a,b,t1,t2) iff for s being Point of () holds b5 . s = (((b - s) * t1) + ((s - a) * t2)) / (b - a) );

theorem Th14: :: TREAL_1:14
for a, b being real number st a < b holds
for t1, t2 being Point of ()
for s being Point of () holds (P (a,b,t1,t2)) . s = (((t2 - t1) / (b - a)) * s) + (((b * t1) - (a * t2)) / (b - a))
proof end;

theorem Th15: :: TREAL_1:15
for a, b being real number st a < b holds
for t1, t2 being Point of () holds P (a,b,t1,t2) is continuous
proof end;

theorem :: TREAL_1:16
for a, b being real number st a < b holds
for t1, t2 being Point of () holds
( (P (a,b,t1,t2)) . ((#) (a,b)) = t1 & (P (a,b,t1,t2)) . ((a,b) (#)) = t2 )
proof end;

theorem :: TREAL_1:17
P (0,1,((#) (0,1)),((0,1) (#))) = id ()
proof end;

theorem Th18: :: TREAL_1:18
for a, b being real number st a < b holds
( id () = (L (((#) (a,b)),((a,b) (#)))) * (P (a,b,((#) (0,1)),((0,1) (#)))) & id () = (P (a,b,((#) (0,1)),((0,1) (#)))) * (L (((#) (a,b)),((a,b) (#)))) )
proof end;

theorem Th19: :: TREAL_1:19
for a, b being real number st a < b holds
( id () = (L (((a,b) (#)),((#) (a,b)))) * (P (a,b,((0,1) (#)),((#) (0,1)))) & id () = (P (a,b,((0,1) (#)),((#) (0,1)))) * (L (((a,b) (#)),((#) (a,b)))) )
proof end;

theorem Th20: :: TREAL_1:20
for a, b being real number st a < b holds
( L (((#) (a,b)),((a,b) (#))) is being_homeomorphism & (L (((#) (a,b)),((a,b) (#)))) " = P (a,b,((#) (0,1)),((0,1) (#))) & P (a,b,((#) (0,1)),((0,1) (#))) is being_homeomorphism & (P (a,b,((#) (0,1)),((0,1) (#)))) " = L (((#) (a,b)),((a,b) (#))) )
proof end;

theorem :: TREAL_1:21
for a, b being real number st a < b holds
( L (((a,b) (#)),((#) (a,b))) is being_homeomorphism & (L (((a,b) (#)),((#) (a,b)))) " = P (a,b,((0,1) (#)),((#) (0,1))) & P (a,b,((0,1) (#)),((#) (0,1))) is being_homeomorphism & (P (a,b,((0,1) (#)),((#) (0,1)))) " = L (((a,b) (#)),((#) (a,b))) )
proof end;

begin

theorem Th22: :: TREAL_1:22
proof end;

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

theorem Th24: :: TREAL_1:24
for f being continuous Function of I,I ex x being Point of I st f . x = x
proof end;

theorem Th25: :: TREAL_1:25
for a, b being real number st a <= b holds
for f being continuous Function of (),() ex x being Point of () st f . x = x
proof end;

theorem Th26: :: TREAL_1:26
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 & [.a,b.] c= the carrier of X & [.a,b.] c= the carrier of Y & f .: [.a,b.] c= [.a,b.] ) holds
ex x being Point of X st f . x = x
proof end;

theorem :: TREAL_1:27
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 & [.a,b.] c= the carrier of X & f .: [.a,b.] c= [.a,b.] ) holds
ex x being Point of X st f . x = x
proof end;