:: The Brouwer Fixed Point Theorem for Intervals
::  by Toshihiko Watanabe
::
:: Received August 17, 1992
:: Copyright (c) 1992-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, XXREAL_1, REAL_1, PRE_TOPC, TOPMETR, XXREAL_0, STRUCT_0,
      SUBSET_1, RCOMP_1, PCOMPS_1, METRIC_1, CARD_1, TARSKI, ARYTM_1, ARYTM_3,
      FUNCT_1, COMPLEX1, SETFAM_1, XBOOLE_0, VALUED_1, BORSUK_1, RELAT_1,
      ORDINAL2, TMAP_1, TOPS_2, RELAT_2, XXREAL_2, SEQ_4, FUNCT_3, TREAL_1,
      FUNCT_2, FUNCT_7;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
      XXREAL_2, XREAL_0, COMPLEX1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
      BINOP_1, REAL_1, SEQ_4, RCOMP_1, PRE_TOPC, TOPS_2, CONNSP_1, METRIC_1,
      DOMAIN_1, STRUCT_0, PCOMPS_1, TOPMETR, TSEP_1, TMAP_1, BORSUK_1;
 constructors REAL_1, SQUARE_1, COMPLEX1, SEQ_4, RCOMP_1, CONNSP_1, TOPS_2,
      TMAP_1, TOPMETR, XXREAL_2, BINOP_2, RVSUM_1, PCOMPS_1, BINOP_1;
 registrations XBOOLE_0, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0,
      MEMBERED, STRUCT_0, PRE_TOPC, METRIC_1, BORSUK_1, TOPMETR, CONNSP_1,
      ORDINAL1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin

:: 1. Properties of Topological Intervals.

reserve a,b,c,d for Real;

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

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

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

theorem :: TREAL_1:4
  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;
  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:5
  0[01] = (#)(0,1) & 1[01] = (0,1)(#);

theorem :: TREAL_1:6
  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 such that
 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
:: TREAL_1:def 3

  for s being Point of Closed-Interval-TSpace(0,1) holds
  it.s = (1-s)*t1 + s*t2;
end;

theorem :: TREAL_1:7
  a <= b implies 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;

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

theorem :: TREAL_1:9
  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:10
  L[01]((#)(0,1),(0,1)(#)) = id Closed-Interval-TSpace(0,1);

definition
  let a,b be Real such that
 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
:: 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);
end;

theorem :: TREAL_1:11
  a < b implies 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);

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

theorem :: TREAL_1:13
  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:14
  P[01](0,1,(#)(0,1),(0,1)(#)) = id Closed-Interval-TSpace(0,1);

theorem :: TREAL_1:15
  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:16
  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:17
  a < b implies
  L[01]((#)(a,b),(a,b)(#)) is being_homeomorphism &
  L[01]((#)(a,b),(a,b)(#))" = P[01](a,b,(#)(0,1),(0,1)(#)) &
  P[01](a,b,(#)(0,1),(0,1)(#)) is being_homeomorphism &
  P[01](a,b,(#)(0,1),(0,1)(#))" = L[01]((#)(a,b),(a,b)(#));

theorem :: TREAL_1:18
  a < b implies
  L[01]((a,b)(#),(#)(a,b)) is being_homeomorphism &
  L[01]((a,b)(#),(#)(a,b))" = P[01](a,b,(0,1)(#),(#)(0,1)) &
  P[01](a,b,(0,1)(#),(#)(0,1)) is being_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:19
  I[01] is connected;

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

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

theorem :: TREAL_1:22
  a <= b implies 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;

theorem :: TREAL_1:23
  for X, Y being non empty SubSpace of R^1, f being continuous Function 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;

::$N Brouwer Fixed Point Theorem for Intervals
theorem :: TREAL_1:24
  for X, Y being non empty SubSpace of R^1, f being continuous Function 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;