BROUWER: Brouwer Fixed Point Theorem for Disks on the Plane

:: Brouwer Fixed Point Theorem for Disks on the Plane
:: by Artur Korni{\l}owicz and Yasunari Shidama
::
:: Received February 22, 2005
:: Copyright (c) 2005-2016 Association of Mizar Users

environ

vocabularies HIDDEN, NUMBERS, EUCLID, SUBSET_1, PRE_TOPC, XBOOLE_0, ZFMISC_1, TARSKI, STRUCT_0, METRIC_1, CARD_1, COMPLEX1, ARYTM_1, RELAT_1, XXREAL_0, CONVEX1, TOPREALB, PROB_1, RVSUM_1, ARYTM_3, SQUARE_1, FUNCT_3, CARD_3, POLYEQ_1, REAL_1, SUPINF_2, MCART_1, FUNCT_1, ABIAN, BORSUK_1, ALGSTR_1, FUNCOP_1, BORSUK_2, ORDINAL2, TOPALG_1, EQREL_1, WAYBEL20, RCOMP_1, TOPREALA, PSCOMP_1, TOPMETR, XXREAL_1, VALUED_1, PARTFUN3, PARTFUN1, TOPS_2, SETFAM_1, BROUWER, FUNCT_2, NAT_1, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, EQREL_1, COMPLEX1, SQUARE_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_3, FUNCOP_1, PSCOMP_1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, RVSUM_1, RCOMP_1, VALUED_1, STRUCT_0, PRE_TOPC, BORSUK_1, TOPS_2, JORDAN1, QUIN_1, POLYEQ_1, BORSUK_2, TOPALG_1, TOPREAL9, TOPALG_2, TOPREALA, TOPREALB, PARTFUN3, ABIAN, XXREAL_0, RLVECT_1, EUCLID;
definitions TARSKI, XBOOLE_0, BORSUK_1, BORSUK_2, TOPALG_2, PSCOMP_1, ABIAN;
theorems TOPRNS_1, XREAL_0, TARSKI, FUNCT_2, TSEP_1, RFUNCT_1, PRE_TOPC, EUCLID, RELAT_1, FUNCT_1, ZFMISC_1, JGRAPH_2, XBOOLE_1, XBOOLE_0, TOPS_2, BORSUK_1, TOPALG_1, EQREL_1, BORSUK_2, FUNCOP_1, TOPMETR, XCMPLX_0, SQUARE_1, XCMPLX_1, FUNCT_3, COMPLEX1, JGRAPH_1, QUIN_1, POLYEQ_1, TOPREAL3, TOPREAL9, TOPALG_2, TOPREALB, BORSUK_5, RCOMP_1, PSCOMP_1, TOPREALA, YELLOW12, TOPGRP_1, PARTFUN3, RVSUM_1, EUCLID_2, XREAL_1, SEQ_2, XXREAL_0, VALUED_1, XXREAL_1, SUBSET_1, JORDAN5A, XTUPLE_0, RLVECT_1;
schemes FUNCT_2;
registrations SUBSET_1, FUNCT_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, MEMBERED, QUIN_1, RCOMP_1, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1, TEX_1, MONOID_0, EUCLID, TOPMETR, PSCOMP_1, BORSUK_2, TOPALG_1, TOPALG_2, TOPREAL9, TOPREALB, PARTFUN3, TOPALG_5, VALUED_0, ZFMISC_1, RELSET_1, PARTFUN4, VALUED_1, RELAT_1, ORDINAL1;
constructors HIDDEN, SQUARE_1, BINOP_2, COMPLEX1, QUIN_1, POLYEQ_1, ABIAN, MONOID_0, TOPALG_1, TOPREAL9, TOPREALA, TOPREALB, PARTFUN3, BORSUK_6, CONVEX1, PSCOMP_1, REAL_1, BINOP_1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities XBOOLE_0, SQUARE_1, BINOP_1, STRUCT_0, RLVECT_1, TOPALG_1;
expansions XBOOLE_0, BORSUK_1, BORSUK_2, TOPALG_2, ABIAN;

set T2 = TOP-REAL 2;

definition

let S, T be non empty TopSpace;

func DiffElems (S,T) -> Subset of [:S,T:] equals :: BROUWER:def 1
{ [s,t] where s is Point of S, t is Point of T : s <> t } ;

coherence

proof end;

end;

:: deftheorem defines DiffElems BROUWER:def 1 :

theorem :: BROUWER:1

for S, T being non empty TopSpace
for x being set holds
( x in DiffElems (S,T) iff ex s being Point of S ex t being Point of T st
( x = [s,t] & s <> t ) ) ;

registration

let S be non trivial TopSpace;
let T be non empty TopSpace;

cluster DiffElems (S,T) -> non empty ;

coherence

proof end;

end;

registration

let S be non empty TopSpace;
let T be non trivial TopSpace;

cluster DiffElems (S,T) -> non empty ;

coherence

proof end;

end;

theorem Th2: :: BROUWER:2

for n being Element of NAT
for x being Point of (TOP-REAL n) holds cl_Ball (x,0) = {x}

proof end;

definition

let n be Nat;
let x be Point of (TOP-REAL n);
let r be Real;

func Tdisk (x,r) -> SubSpace of TOP-REAL n equals :: BROUWER:def 2
(TOP-REAL n) | (cl_Ball (x,r));

coherence ;

end;

:: deftheorem defines Tdisk BROUWER:def 2 :

registration

let n be Nat;
let x be Point of (TOP-REAL n);
let r be non negative Real;

cluster Tdisk (x,r) -> non empty ;

coherence ;

end;

theorem Th3: :: BROUWER:3

for n being Element of NAT
for r being Real
for x being Point of (TOP-REAL n) holds the carrier of (Tdisk (x,r)) = cl_Ball (x,r)

proof end;

registration

let n be Element of NAT ;
let x be Point of (TOP-REAL n);
let r be Real;

cluster Tdisk (x,r) -> convex ;

coherence by Th3;

end;

theorem Th4: :: BROUWER:4

for n being Element of NAT
for r being non negative Real
for s, t, x being Point of (TOP-REAL n) st s <> t & s is Point of (Tdisk (x,r)) & s is not Point of (Tcircle (x,r)) holds
ex e being Point of (Tcircle (x,r)) st {e} = (halfline (s,t)) /\ (Sphere (x,r))

proof end;

theorem Th5: :: BROUWER:5

for n being Element of NAT
for r being non negative Real
for s, t, x being Point of (TOP-REAL n) st s <> t & s in the carrier of (Tcircle (x,r)) & t is Point of (Tdisk (x,r)) holds
ex e being Point of (Tcircle (x,r)) st
( e <> s & {s,e} = (halfline (s,t)) /\ (Sphere (x,r)) )

proof end;

definition

let n be non zero Element of NAT ;
let o be Point of (TOP-REAL n);
let s, t be Point of (TOP-REAL n);
let r be non negative Real;
assume that
A1: s is Point of (Tdisk (o,r)) and
A2: t is Point of (Tdisk (o,r)) and
A3: s <> t ;

func HC (s,t,o,r) -> Point of (TOP-REAL n) means :Def3: :: BROUWER:def 3
( it in (halfline (s,t)) /\ (Sphere (o,r)) & it <> s );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines HC BROUWER:def 3 :

theorem Th6: :: BROUWER:6

for r being non negative Real
for n being non zero Element of NAT
for s, t, o being Point of (TOP-REAL n) st s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t holds
HC (s,t,o,r) is Point of (Tcircle (o,r))

proof end;

theorem :: BROUWER:7

for a being Real
for r being non negative Real
for n being non zero Element of NAT
for s, t, o being Point of (TOP-REAL n)
for S, T, O being Element of REAL n st S = s & T = t & O = o & s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t & a = ((- |((t - s),(s - o))|) + (sqrt ((|((t - s),(s - o))| ^2) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2)))))) / (Sum (sqr (T - S))) holds
HC (s,t,o,r) = ((1 - a) * s) + (a * t)

proof end;

theorem Th8: :: BROUWER:8

for a being Real
for r being non negative Real
for r1, r2, s1, s2 being Real
for s, t, o being Point of (TOP-REAL 2) st s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t & r1 = (t `1) - (s `1) & r2 = (t `2) - (s `2) & s1 = (s `1) - (o `1) & s2 = (s `2) - (o `2) & a = ((- ((s1 * r1) + (s2 * r2))) + (sqrt ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2)))))) / ((r1 ^2) + (r2 ^2)) holds
HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]|

proof end;

definition

let n be non zero Element of NAT ;
let o be Point of (TOP-REAL n);
let r be non negative Real;
let x be Point of (Tdisk (o,r));
let f be Function of (Tdisk (o,r)),(Tdisk (o,r));
assume A1: not x is_a_fixpoint_of f ;

func HC (x,f) -> Point of (Tcircle (o,r)) means :Def4: :: BROUWER:def 4
ex y, z being Point of (TOP-REAL n) st
( y = x & z = f . x & it = HC (z,y,o,r) );

existence

proof end;

uniqueness ;

end;

:: deftheorem Def4 defines HC BROUWER:def 4 :

theorem Th9: :: BROUWER:9

for r being non negative Real
for n being non zero Element of NAT
for o being Point of (TOP-REAL n)
for x being Point of (Tdisk (o,r))
for f being Function of (Tdisk (o,r)),(Tdisk (o,r)) st not x is_a_fixpoint_of f & x is Point of (Tcircle (o,r)) holds
HC (x,f) = x

proof end;

theorem Th10: :: BROUWER:10

for r being positive Real
for o being Point of (TOP-REAL 2)
for Y being non empty SubSpace of Tdisk (o,r) st Y = Tcircle (o,r) holds
not Y is_a_retract_of Tdisk (o,r)

proof end;

definition

let n be non zero Element of NAT ;
let r be non negative Real;
let o be Point of (TOP-REAL n);
let f be Function of (Tdisk (o,r)),(Tdisk (o,r));

func BR-map f -> Function of (Tdisk (o,r)),(Tcircle (o,r)) means :Def5: :: BROUWER:def 5
for x being Point of (Tdisk (o,r)) holds it . x = HC (x,f);

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines BR-map BROUWER:def 5 :

theorem Th11: :: BROUWER:11

proof end;

theorem :: BROUWER:12

for r being non negative Real
for n being non zero Element of NAT
for o being Point of (TOP-REAL n)
for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f is without_fixpoints holds
(BR-map f) | (Sphere (o,r)) = id (Tcircle (o,r))

proof end;

Lm1: now :: thesis:

let T be non empty TopSpace; :: thesis:
let a be Element of REAL ; :: thesis:
set c = the carrier of T;
set f = the carrier of T --> a;
thus the carrier of T --> a is continuous :: thesis:

proof

let Y be Subset of REAL; :: according to PSCOMP_1:def 3 :: thesis:
A1: dom ( the carrier of T --> a) = the carrier of T by FUNCT_2:def 1;
assume Y is closed ; :: thesis:
A2: rng ( the carrier of T --> a) = {a} by FUNCOP_1:8;

per cases ;

suppose a in Y ; :: thesis:

then A3: rng ( the carrier of T --> a) c= Y by A2, ZFMISC_1:31;
( the carrier of T --> a) " Y = ( the carrier of T --> a) " ((rng ( the carrier of T --> a)) /\ Y) by RELAT_1:133
.= ( the carrier of T --> a) " (rng ( the carrier of T --> a)) by A3, XBOOLE_1:28
.= [#] T by A1, RELAT_1:134 ;
hence ( the carrier of T --> a) " Y is closed ; :: thesis:

end;

suppose not a in Y ; :: thesis:

then A4: rng ( the carrier of T --> a) misses Y by A2, ZFMISC_1:50;
( the carrier of T --> a) " Y = ( the carrier of T --> a) " ((rng ( the carrier of T --> a)) /\ Y) by RELAT_1:133
.= ( the carrier of T --> a) " {} by A4
.= {} T ;
hence ( the carrier of T --> a) " Y is closed ; :: thesis:

end;

theorem Th13: :: BROUWER:13

for r being positive Real
for o being Point of (TOP-REAL 2)
for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f is without_fixpoints holds
BR-map f is continuous

proof end;

Brouwer Fixed Point Theorem

theorem Th14: :: BROUWER:14

for r being non negative Real
for o being Point of (TOP-REAL 2)
for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) holds f is with_fixpoint

proof end;

Brouwer Fixed Point Theorem for Disks on the Plane

theorem :: BROUWER:15

for r being non negative Real
for o being Point of (TOP-REAL 2)
for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) ex x being Point of (Tdisk (o,r)) st f . x = x

proof end;