:: by Artur Korni{\l}owicz and Yasunari Shidama

::

:: Received February 22, 2005

:: Copyright (c) 2005 Association of Mizar Users

begin

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

{ [s,t] where s is Point of S, t is Point of T : s <> t } is Subset of [:S,T:]

end;
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

{ [s,t] where s is Point of S, t is Point of T : s <> t } is Subset of [:S,T:]

proof end;

:: deftheorem defines DiffElems BROUWER:def 1 :

for S, T being non empty TopSpace holds DiffElems (S,T) = { [s,t] where s is Point of S, t is Point of T : s <> t } ;

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 ) ) ;

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 empty non trivial TopSpace;

let T be non empty TopSpace;

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

coherence

not DiffElems (S,T) is empty

end;
let T be non empty TopSpace;

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

coherence

not DiffElems (S,T) is empty

proof end;

registration

let S be non empty TopSpace;

let T be non empty non trivial TopSpace;

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

coherence

not DiffElems (S,T) is empty

end;
let T be non empty non trivial TopSpace;

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

coherence

not DiffElems (S,T) is empty

proof end;

theorem Th2: :: BROUWER:2

proof end;

definition

let n be Element of NAT ;

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

let r be real number ;

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

(TOP-REAL n) | (cl_Ball (x,r));

coherence

(TOP-REAL n) | (cl_Ball (x,r)) is SubSpace of TOP-REAL n ;

end;
let x be Point of (TOP-REAL n);

let r be real number ;

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

(TOP-REAL n) | (cl_Ball (x,r));

coherence

(TOP-REAL n) | (cl_Ball (x,r)) is SubSpace of TOP-REAL n ;

:: deftheorem defines Tdisk BROUWER:def 2 :

for n being Element of NAT

for x being Point of (TOP-REAL n)

for r being real number holds Tdisk (x,r) = (TOP-REAL n) | (cl_Ball (x,r));

registration

let n be Element of NAT ;

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

let r be non negative real number ;

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

coherence

not Tdisk (x,r) is empty ;

end;
let x be Point of (TOP-REAL n);

let r be non negative real number ;

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

coherence

not Tdisk (x,r) is empty ;

theorem Th3: :: BROUWER:3

for n being Element of NAT

for r being real number

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

for r being real number

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 number ;

cluster Tdisk (x,r) -> convex ;

coherence

Tdisk (x,r) is convex

end;
let x be Point of (TOP-REAL n);

let r be real number ;

cluster Tdisk (x,r) -> convex ;

coherence

Tdisk (x,r) is convex

proof end;

theorem Th4: :: BROUWER:4

for n being Element of NAT

for r being non negative real number

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))

for r being non negative real number

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 number

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)) )

for r being non negative real number

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 empty 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 number ;

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

ex b_{1} being Point of (TOP-REAL n) st

( b_{1} in (halfline (s,t)) /\ (Sphere (o,r)) & b_{1} <> s )

for b_{1}, b_{2} being Point of (TOP-REAL n) st b_{1} in (halfline (s,t)) /\ (Sphere (o,r)) & b_{1} <> s & b_{2} in (halfline (s,t)) /\ (Sphere (o,r)) & b_{2} <> s holds

b_{1} = b_{2}

end;
let o be Point of (TOP-REAL n);

let s, t be Point of (TOP-REAL n);

let r be non negative real number ;

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

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines HC BROUWER:def 3 :

for n being non empty Element of NAT

for o, s, t being Point of (TOP-REAL n)

for r being non negative real number st s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t holds

for b

( b

theorem Th6: :: BROUWER:6

for r being non negative real number

for n being non empty Element of NAT

for s, o, t 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))

for n being non empty Element of NAT

for s, o, t 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 number

for r being non negative real number

for n being non empty 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)

for r being non negative real number

for n being non empty 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 number

for r being non negative real number

for r1, r2, s1, s2 being real number

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))]|

for r being non negative real number

for r1, r2, s1, s2 being real number

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 empty Element of NAT ;

let o be Point of (TOP-REAL n);

let r be non negative real number ;

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

ex b_{1} being Point of (Tcircle (o,r)) ex y, z being Point of (TOP-REAL n) st

( y = x & z = f . x & b_{1} = HC (z,y,o,r) )

for b_{1}, b_{2} being Point of (Tcircle (o,r)) st ex y, z being Point of (TOP-REAL n) st

( y = x & z = f . x & b_{1} = HC (z,y,o,r) ) & ex y, z being Point of (TOP-REAL n) st

( y = x & z = f . x & b_{2} = HC (z,y,o,r) ) holds

b_{1} = b_{2}
;

end;
let o be Point of (TOP-REAL n);

let r be non negative real number ;

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

ex b

( y = x & z = f . x & b

proof end;

uniqueness for b

( y = x & z = f . x & b

( y = x & z = f . x & b

b

:: deftheorem Def4 defines HC BROUWER:def 4 :

for n being non empty Element of NAT

for o being Point of (TOP-REAL n)

for r being non negative real number

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 holds

for b

( b

( y = x & z = f . x & b

theorem Th9: :: BROUWER:9

for r being non negative real number

for n being non empty 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

for n being non empty 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 number

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)

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 empty Element of NAT ;

let r be non negative real number ;

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

ex b_{1} being Function of (Tdisk (o,r)),(Tcircle (o,r)) st

for x being Point of (Tdisk (o,r)) holds b_{1} . x = HC (x,f)

for b_{1}, b_{2} being Function of (Tdisk (o,r)),(Tcircle (o,r)) st ( for x being Point of (Tdisk (o,r)) holds b_{1} . x = HC (x,f) ) & ( for x being Point of (Tdisk (o,r)) holds b_{2} . x = HC (x,f) ) holds

b_{1} = b_{2}

end;
let r be non negative real number ;

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

ex b

for x being Point of (Tdisk (o,r)) holds b

proof end;

uniqueness for b

b

proof end;

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

for n being non empty Element of NAT

for r being non negative real number

for o being Point of (TOP-REAL n)

for f being Function of (Tdisk (o,r)),(Tdisk (o,r))

for b

( b

theorem Th11: :: BROUWER:11

for r being non negative real number

for n being non empty 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

(BR-map f) . x = x

for n being non empty 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

(BR-map f) . x = x

proof end;

theorem :: BROUWER:12

for r being non negative real number

for n being non empty 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 has_no_fixpoint holds

(BR-map f) | (Sphere (o,r)) = id (Tcircle (o,r))

for n being non empty 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 has_no_fixpoint holds

(BR-map f) | (Sphere (o,r)) = id (Tcircle (o,r))

proof end;

Lm1: now

let T be non empty TopSpace; :: thesis: for a being Real holds the carrier of T --> a is continuous

let a be Real; :: thesis: the carrier of T --> a is continuous

set c = the carrier of T;

set f = the carrier of T --> a;

thus the carrier of T --> a is continuous :: thesis: verum

end;
let a be Real; :: thesis: the carrier of T --> a is continuous

set c = the carrier of T;

set f = the carrier of T --> a;

thus the carrier of T --> a is continuous :: thesis: verum

proof

let Y be Subset of REAL; :: according to PSCOMP_1:def 25 :: thesis: ( not Y is closed or ( the carrier of T --> a) " Y is closed )

A1: dom ( the carrier of T --> a) = the carrier of T by FUNCT_2:def 1;

assume Y is closed ; :: thesis: ( the carrier of T --> a) " Y is closed

A2: rng ( the carrier of T --> a) = {a} by FUNCOP_1:14;

end;
A1: dom ( the carrier of T --> a) = the carrier of T by FUNCT_2:def 1;

assume Y is closed ; :: thesis: ( the carrier of T --> a) " Y is closed

A2: rng ( the carrier of T --> a) = {a} by FUNCOP_1:14;

per cases
( a in Y or not a in Y )
;

end;

suppose
a in Y
; :: thesis: ( the carrier of T --> a) " Y is closed

then A3:
rng ( the carrier of T --> a) c= Y
by A2, ZFMISC_1:37;

( the carrier of T --> a) " Y = ( the carrier of T --> a) " ((rng ( the carrier of T --> a)) /\ Y) by RELAT_1:168

.= ( the carrier of T --> a) " (rng ( the carrier of T --> a)) by A3, XBOOLE_1:28

.= [#] T by A1, RELAT_1:169 ;

hence ( the carrier of T --> a) " Y is closed ; :: thesis: verum

end;
( the carrier of T --> a) " Y = ( the carrier of T --> a) " ((rng ( the carrier of T --> a)) /\ Y) by RELAT_1:168

.= ( the carrier of T --> a) " (rng ( the carrier of T --> a)) by A3, XBOOLE_1:28

.= [#] T by A1, RELAT_1:169 ;

hence ( the carrier of T --> a) " Y is closed ; :: thesis: verum

suppose
not a in Y
; :: thesis: ( the carrier of T --> a) " Y is closed

then A4:
rng ( the carrier of T --> a) misses Y
by A2, ZFMISC_1:56;

( the carrier of T --> a) " Y = ( the carrier of T --> a) " ((rng ( the carrier of T --> a)) /\ Y) by RELAT_1:168

.= ( the carrier of T --> a) " {} by A4, XBOOLE_0:def 7

.= {} T by RELAT_1:171 ;

hence ( the carrier of T --> a) " Y is closed ; :: thesis: verum

end;
( the carrier of T --> a) " Y = ( the carrier of T --> a) " ((rng ( the carrier of T --> a)) /\ Y) by RELAT_1:168

.= ( the carrier of T --> a) " {} by A4, XBOOLE_0:def 7

.= {} T by RELAT_1:171 ;

hence ( the carrier of T --> a) " Y is closed ; :: thesis: verum

theorem Th13: :: BROUWER:13

for r being positive real number

for o being Point of (TOP-REAL 2)

for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f has_no_fixpoint holds

BR-map f is continuous

for o being Point of (TOP-REAL 2)

for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f has_no_fixpoint holds

BR-map f is continuous

proof end;

theorem Th14: :: BROUWER:14

for r being non negative real number

for o being Point of (TOP-REAL 2)

for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) holds f has_a_fixpoint

for o being Point of (TOP-REAL 2)

for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) holds f has_a_fixpoint

proof end;

theorem :: BROUWER:15

for r being non negative real number

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

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;