Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

### The Brouwer Fixed Point Theorem for Intervals

by
Toshihiko Watanabe

MML identifier: TREAL_1
[ Mizar article, MML identifier index ]

```environ

vocabulary ARYTM, RCOMP_1, BOOLE, PRE_TOPC, TOPMETR, PCOMPS_1, METRIC_1,
SUBSET_1, ARYTM_1, FUNCT_1, ABSVALUE, TARSKI, SETFAM_1, SEQ_1, BORSUK_1,
TMAP_1, RELAT_1, ORDINAL2, ARYTM_3, TOPS_2, RELAT_2, SEQ_2, SEQ_4,
SQUARE_1, FUNCT_3, TREAL_1;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
RELAT_1, FUNCT_1, FUNCT_2, ABSVALUE, REAL_1, SQUARE_1, SEQ_4, RCOMP_1,
PRE_TOPC, TOPS_2, CONNSP_1, METRIC_1, GRCAT_1, STRUCT_0, PCOMPS_1,
TOPMETR, TSEP_1, TMAP_1, BORSUK_1;
constructors ABSVALUE, REAL_1, SQUARE_1, SEQ_4, RCOMP_1, TOPS_2, CONNSP_1,
GRCAT_1, TOPMETR, TMAP_1, PARTFUN1, MEMBERED;
clusters SUBSET_1, FUNCT_1, PRE_TOPC, TOPMETR, BORSUK_1, STRUCT_0, XREAL_0,
METRIC_1, RELSET_1, MEMBERED, ZFMISC_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;

begin
:: 1. Properties of Topological Intervals.

reserve a,b,c,d for real number;

theorem :: TREAL_1:1
a <= c & d <= b implies [.c,d.] c= [.a,b.];

theorem :: TREAL_1:2
a <= c & b <= d & c <= b implies [.a,b.] \/ [.c,d.] = [.a,d.];

theorem :: TREAL_1:3
a <= c & b <= d & c <= b implies [.a,b.] /\ [.c,d.] = [.c,b.];

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

theorem :: TREAL_1:5
a <= b implies Closed-Interval-TSpace(a,b) is closed SubSpace of R^1;

theorem :: TREAL_1:6
a <= c & d <= b & c <= d implies
Closed-Interval-TSpace(c,d) is closed SubSpace of Closed-Interval-TSpace(a,b);

theorem :: TREAL_1:7
a <= c & b <= d & c <= b implies
Closed-Interval-TSpace(a,d) =
Closed-Interval-TSpace(a,b) union Closed-Interval-TSpace(c,d) &
Closed-Interval-TSpace(c,b) =
Closed-Interval-TSpace(a,b) meet Closed-Interval-TSpace(c,d);

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

theorem :: TREAL_1:8
0 = (#)(0,1) & 1 = (0,1)(#);

theorem :: TREAL_1:9
a <= b & b <= c implies (#)(a,b) = (#)(a,c) & (b,c)(#) = (a,c)(#);

begin
:: 2. Continuous Mappings Between Topological Intervals.

definition let a,b be real number such that  a <= b;
let t1,t2 be Point of Closed-Interval-TSpace(a,b);
func L(t1,t2) -> map of
Closed-Interval-TSpace(0,1),Closed-Interval-TSpace(a,b) means
:: TREAL_1:def 3
for s being Point of Closed-Interval-TSpace(0,1),
r,r1,r2 being real number st
s=r & r1=t1 & r2=t2 holds it.s = (1-r)*r1 + r*r2;
end;

theorem :: TREAL_1:10
a <= b implies
for t1,t2 being Point of Closed-Interval-TSpace(a,b) holds
for s being Point of Closed-Interval-TSpace(0,1),
r,r1,r2 being real number st
s=r & r1=t1 & r2=t2 holds L(t1,t2).s = (r2 - r1)*r + r1;

theorem :: TREAL_1:11
a <= b implies
for t1,t2 being Point of Closed-Interval-TSpace(a,b) holds
L(t1,t2) is continuous map of
Closed-Interval-TSpace(0,1),Closed-Interval-TSpace(a,b);

theorem :: TREAL_1:12
a <= b implies
for t1,t2 being Point of Closed-Interval-TSpace(a,b) holds
L(t1,t2).(#)(0,1) = t1 & L(t1,t2).(0,1)(#) = t2;

theorem :: TREAL_1:13
L((#)(0,1),(0,1)(#)) = id Closed-Interval-TSpace(0,1);

definition let a,b be real number such that  a < b;
let t1,t2 be Point of Closed-Interval-TSpace(0,1);
func P(a,b,t1,t2) -> map of
Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(0,1) means
:: TREAL_1:def 4
for s being Point of Closed-Interval-TSpace(a,b),
r,r1,r2 being real number st
s=r & r1=t1 & r2=t2 holds it.s = ((b-r)*r1 + (r-a)*r2)/(b-a);
end;

theorem :: TREAL_1:14
a < b implies
for t1,t2 being Point of Closed-Interval-TSpace(0,1)
for s being Point of Closed-Interval-TSpace(a,b), r,r1,r2 being Real st
s=r & r1=t1 & r2=t2 holds
P(a,b,t1,t2).s = ((r2 - r1)/(b-a))*r + (b*r1 -a*r2)/(b-a);

theorem :: TREAL_1:15
a < b implies
for t1,t2 being Point of Closed-Interval-TSpace(0,1) holds
P(a,b,t1,t2) is continuous map of
Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(0,1);

theorem :: TREAL_1:16
a < b implies
for t1,t2 being Point of Closed-Interval-TSpace(0,1) holds
P(a,b,t1,t2).(#)(a,b) = t1 & P(a,b,t1,t2).(a,b)(#) = t2;

theorem :: TREAL_1:17
P(0,1,(#)(0,1),(0,1)(#)) = id Closed-Interval-TSpace(0,1);

theorem :: TREAL_1:18
a < b implies
id Closed-Interval-TSpace(a,b) =
L((#)(a,b),(a,b)(#)) * P(a,b,(#)(0,1),(0,1)(#)) &
id Closed-Interval-TSpace(0,1) =
P(a,b,(#)(0,1),(0,1)(#)) * L((#)(a,b),(a,b)(#));

theorem :: TREAL_1:19
a < b implies
id Closed-Interval-TSpace(a,b) =
L((a,b)(#),(#)(a,b)) * P(a,b,(0,1)(#),(#)(0,1)) &
id Closed-Interval-TSpace(0,1) =
P(a,b,(0,1)(#),(#)(0,1)) * L((a,b)(#),(#)(a,b));

theorem :: TREAL_1:20
a < b implies
L((#)(a,b),(a,b)(#)) is_homeomorphism &
L((#)(a,b),(a,b)(#))" = P(a,b,(#)(0,1),(0,1)(#)) &
P(a,b,(#)(0,1),(0,1)(#)) is_homeomorphism &
P(a,b,(#)(0,1),(0,1)(#))" = L((#)(a,b),(a,b)(#));

theorem :: TREAL_1:21
a < b implies
L((a,b)(#),(#)(a,b)) is_homeomorphism &
L((a,b)(#),(#)(a,b))" = P(a,b,(0,1)(#),(#)(0,1)) &
P(a,b,(0,1)(#),(#)(0,1)) is_homeomorphism &
P(a,b,(0,1)(#),(#)(0,1))" = L((a,b)(#),(#)(a,b));

begin
:: 3. Connectedness of Intervals and Brouwer Fixed Point Theorem for Intervals.

theorem :: TREAL_1:22
I is connected;

theorem :: TREAL_1:23
a <= b implies Closed-Interval-TSpace(a,b) is connected;

theorem :: TREAL_1:24
for f being continuous map of I,I
ex x being Point of I st f.x = x;

theorem :: TREAL_1:25
a <= b implies
for f being continuous map
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;

theorem :: TREAL_1:26
for X, Y being non empty SubSpace of R^1, f being continuous map of X,Y
holds
(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.]) implies
ex x being Point of X st f.x = x;

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