:: The Brouwer Fixed Point Theorem for Intervals :: by Toshihiko Watanabe :: :: Received August 17, 1992 :: Copyright (c) 1992-2018 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;