The abstract of the Mizar article:

The Brouwer Fixed Point Theorem for Intervals

by

Toshihiko Watanabe

Received August 17, 1992

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[01] = (#)(0,1) & 1[01] = (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[01](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[01](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[01](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[01](t1,t2).(#)(0,1) = t1 & L[01](t1,t2).(0,1)(#) = t2;

theorem :: TREAL_1:13
   L[01]((#)(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[01](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[01](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[01](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[01](a,b,t1,t2).(#)(a,b) = t1 & P[01](a,b,t1,t2).(a,b)(#) = t2;

theorem :: TREAL_1:17
   P[01](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[01]((#)(a,b),(a,b)(#)) * P[01](a,b,(#)(0,1),(0,1)(#)) &
  id Closed-Interval-TSpace(0,1) =
        P[01](a,b,(#)(0,1),(0,1)(#)) * L[01]((#)(a,b),(a,b)(#));

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

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

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

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

theorem :: TREAL_1:22
 I[01] 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[01],I[01]
  ex x being Point of I[01] 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;