:: by Karol P\kak

::

:: Received February 11, 2014

:: Copyright (c) 2014-2016 Association of Mizar Users

Lm1: for n being Nat

for V being Subset of (TopSpaceMetr (Euclid n)) st V is open holds

for e being Point of (Euclid n) st e in V holds

ex r being Real st

( r > 0 & OpenHypercube (e,r) c= V )

proof end;

Lm2: for n being Nat

for p being Point of (TOP-REAL n)

for r being Real st r > 0 holds

( not cl_Ball (p,r) is boundary & cl_Ball (p,r) is compact )

proof end;

registration

let X be set ;

let n be Nat;

for b_{1} being Function of X,(TOP-REAL n) holds b_{1} is FinSequence-yielding

end;
let n be Nat;

cluster Function-like quasi_total -> FinSequence-yielding for Element of K10(K11(X, the carrier of (TOP-REAL n)));

coherence for b

proof end;

definition

let X be set ;

let n, m be Nat;

let f be Function of X,(TOP-REAL n);

let g be Function of X,(TOP-REAL m);

:: original: ^^

redefine func f ^^ g -> Function of X,(TOP-REAL (n + m));

coherence

f ^^ g is Function of X,(TOP-REAL (n + m))

end;
let n, m be Nat;

let f be Function of X,(TOP-REAL n);

let g be Function of X,(TOP-REAL m);

:: original: ^^

redefine func f ^^ g -> Function of X,(TOP-REAL (n + m));

coherence

f ^^ g is Function of X,(TOP-REAL (n + m))

proof end;

registration

let T be TopSpace;

let n, m be Nat;

let f be continuous Function of T,(TOP-REAL n);

let g be continuous Function of T,(TOP-REAL m);

coherence

for b_{1} being Function of T,(TOP-REAL (n + m)) st b_{1} = f ^^ g holds

b_{1} is continuous

end;
let n, m be Nat;

let f be continuous Function of T,(TOP-REAL n);

let g be continuous Function of T,(TOP-REAL m);

coherence

for b

b

proof end;

definition

let f be real-valued Function;

ex b_{1} being Function st

( dom b_{1} = dom f & ( for x being object st x in dom b_{1} holds

b_{1} . x = |[(f . x)]| ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom f & ( for x being object st x in dom b_{1} holds

b_{1} . x = |[(f . x)]| ) & dom b_{2} = dom f & ( for x being object st x in dom b_{2} holds

b_{2} . x = |[(f . x)]| ) holds

b_{1} = b_{2}

end;
func |[f]| -> Function means :Def1: :: BROUWER3:def 1

( dom it = dom f & ( for x being object st x in dom it holds

it . x = |[(f . x)]| ) );

existence ( dom it = dom f & ( for x being object st x in dom it holds

it . x = |[(f . x)]| ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines |[ BROUWER3:def 1 :

for f being real-valued Function

for b_{2} being Function holds

( b_{2} = |[f]| iff ( dom b_{2} = dom f & ( for x being object st x in dom b_{2} holds

b_{2} . x = |[(f . x)]| ) ) );

for f being real-valued Function

for b

( b

b

registration
end;

definition

let X be set ;

let Y be non empty real-membered set ;

let f be Function of X,Y;

:: original: |[

redefine func |[f]| -> Function of X,(TOP-REAL 1);

coherence

|[f]| is Function of X,(TOP-REAL 1)

end;
let Y be non empty real-membered set ;

let f be Function of X,Y;

:: original: |[

redefine func |[f]| -> Function of X,(TOP-REAL 1);

coherence

|[f]| is Function of X,(TOP-REAL 1)

proof end;

registration

let T be non empty TopSpace;

let f be continuous Function of T,R^1;

coherence

for b_{1} being Function of T,(TOP-REAL 1) st b_{1} = |[f]| holds

b_{1} is continuous

end;
let f be continuous Function of T,R^1;

coherence

for b

b

proof end;

registration

let T be non empty TopSpace;

let f be continuous RealMap of T;

coherence

for b_{1} being Function of T,(TOP-REAL 1) st b_{1} = |[f]| holds

b_{1} is continuous

end;
let f be continuous RealMap of T;

coherence

for b

b

proof end;

theorem Th1: :: BROUWER3:1

for N being non zero Nat

for F being Element of N -tuples_on (Funcs ( the carrier of (TOP-REAL (N + 1)), the carrier of R^1)) st ( for i being Nat st i in dom F holds

F . i = PROJ ((N + 1),i) ) holds

( ( for t being Point of (TOP-REAL (N + 1)) holds <:F:> . t = t | N ) & ( for Sp, Sn being Subset of (TOP-REAL (N + 1)) st Sp = { u where u is Point of (TOP-REAL (N + 1)) : ( u . (N + 1) >= 0 & |.u.| = 1 ) } & Sn = { t where t is Point of (TOP-REAL (N + 1)) : ( t . (N + 1) <= 0 & |.t.| = 1 ) } holds

( <:F:> .: Sp = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: Sn = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: (Sp /\ Sn) = Sphere ((0. (TOP-REAL N)),1) & ( for H being Function of ((TOP-REAL (N + 1)) | Sp),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sp holds

H is being_homeomorphism ) & ( for H being Function of ((TOP-REAL (N + 1)) | Sn),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sn holds

H is being_homeomorphism ) ) ) )

for F being Element of N -tuples_on (Funcs ( the carrier of (TOP-REAL (N + 1)), the carrier of R^1)) st ( for i being Nat st i in dom F holds

F . i = PROJ ((N + 1),i) ) holds

( ( for t being Point of (TOP-REAL (N + 1)) holds <:F:> . t = t | N ) & ( for Sp, Sn being Subset of (TOP-REAL (N + 1)) st Sp = { u where u is Point of (TOP-REAL (N + 1)) : ( u . (N + 1) >= 0 & |.u.| = 1 ) } & Sn = { t where t is Point of (TOP-REAL (N + 1)) : ( t . (N + 1) <= 0 & |.t.| = 1 ) } holds

( <:F:> .: Sp = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: Sn = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: (Sp /\ Sn) = Sphere ((0. (TOP-REAL N)),1) & ( for H being Function of ((TOP-REAL (N + 1)) | Sp),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sp holds

H is being_homeomorphism ) & ( for H being Function of ((TOP-REAL (N + 1)) | Sn),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sn holds

H is being_homeomorphism ) ) ) )

proof end;

theorem Th2: :: BROUWER3:2

for n being Nat

for Sp, Sn being Subset of (TOP-REAL n) st Sp = { s where s is Point of (TOP-REAL n) : ( s . n >= 0 & |.s.| = 1 ) } & Sn = { t where t is Point of (TOP-REAL n) : ( t . n <= 0 & |.t.| = 1 ) } holds

( Sp is closed & Sn is closed )

for Sp, Sn being Subset of (TOP-REAL n) st Sp = { s where s is Point of (TOP-REAL n) : ( s . n >= 0 & |.s.| = 1 ) } & Sn = { t where t is Point of (TOP-REAL n) : ( t . n <= 0 & |.t.| = 1 ) } holds

( Sp is closed & Sn is closed )

proof end;

theorem Th3: :: BROUWER3:3

for n being Nat

for TM being metrizable TopSpace st TM is finite-ind & TM is second-countable holds

for F being closed Subset of TM st ind (F `) <= n holds

for f being continuous Function of (TM | F),(Tunit_circle (n + 1)) ex g being continuous Function of TM,(Tunit_circle (n + 1)) st g | F = f

for TM being metrizable TopSpace st TM is finite-ind & TM is second-countable holds

for F being closed Subset of TM st ind (F `) <= n holds

for f being continuous Function of (TM | F),(Tunit_circle (n + 1)) ex g being continuous Function of TM,(Tunit_circle (n + 1)) st g | F = f

proof end;

theorem Th4: :: BROUWER3:4

for n being Nat

for p being Point of (TOP-REAL n)

for A being Subset of (TOP-REAL n)

for r being Real st not p in A & r > 0 holds

ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | (Sphere (p,r))) st

( h is continuous & h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) )

for p being Point of (TOP-REAL n)

for A being Subset of (TOP-REAL n)

for r being Real st not p in A & r > 0 holds

ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | (Sphere (p,r))) st

( h is continuous & h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) )

proof end;

theorem Th5: :: BROUWER3:5

for n being Nat

for p, q being Point of (TOP-REAL n)

for r, s being Real st r + |.(p - q).| <= s holds

Ball (p,r) c= Ball (q,s)

for p, q being Point of (TOP-REAL n)

for r, s being Real st r + |.(p - q).| <= s holds

Ball (p,r) c= Ball (q,s)

proof end;

:: The Small Inductive Dimension of the Sphere

theorem Th7: :: BROUWER3:7

for n being Nat

for p being Point of (TOP-REAL n)

for r being Real st r > 0 holds

ind (Sphere (p,r)) = n - 1

for p being Point of (TOP-REAL n)

for r being Real st r > 0 holds

ind (Sphere (p,r)) = n - 1

proof end;

:: in Terms of Continuous Transformations

theorem Th8: :: BROUWER3:8

for n being Nat

for A being Subset of (TOP-REAL n)

for p being Point of (TOP-REAL n) st n > 0 & p in A & ( for r being Real st r > 0 holds

ex U being open Subset of ((TOP-REAL n) | A) st

( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(Tunit_circle n) st f is continuous holds

ex h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st

( h is continuous & h | (A \ U) = f ) ) ) ) holds

p in Fr A

for A being Subset of (TOP-REAL n)

for p being Point of (TOP-REAL n) st n > 0 & p in A & ( for r being Real st r > 0 holds

ex U being open Subset of ((TOP-REAL n) | A) st

( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(Tunit_circle n) st f is continuous holds

ex h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st

( h is continuous & h | (A \ U) = f ) ) ) ) holds

p in Fr A

proof end;

theorem Th9: :: BROUWER3:9

for n being Nat

for A being Subset of (TOP-REAL n)

for p being Point of (TOP-REAL n) st p in Fr A & A is closed holds

for r being Real st r > 0 holds

ex U being open Subset of ((TOP-REAL n) | A) st

( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(Tunit_circle n) st f is continuous holds

ex h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st

( h is continuous & h | (A \ U) = f ) ) )

for A being Subset of (TOP-REAL n)

for p being Point of (TOP-REAL n) st p in Fr A & A is closed holds

for r being Real st r > 0 holds

ex U being open Subset of ((TOP-REAL n) | A) st

( p in U & U c= Ball (p,r) & ( for f being Function of ((TOP-REAL n) | (A \ U)),(Tunit_circle n) st f is continuous holds

ex h being Function of ((TOP-REAL n) | A),(Tunit_circle n) st

( h is continuous & h | (A \ U) = f ) ) )

proof end;

Lm3: for n being Nat

for A, B being Subset of (TOP-REAL n) st n = 0 holds

for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds

for p being Point of (TOP-REAL n) holds

( ( p in Fr A implies h . p in Fr B ) & ( p in Int A implies h . p in Int B ) )

proof end;

theorem Th10: :: BROUWER3:10

for n being Nat

for p being Point of (TOP-REAL n)

for A, B being Subset of (TOP-REAL n) st A is closed & p in Fr A holds

for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds

h . p in Fr B

for p being Point of (TOP-REAL n)

for A, B being Subset of (TOP-REAL n) st A is closed & p in Fr A holds

for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds

h . p in Fr B

proof end;

theorem Th11: :: BROUWER3:11

for n being Nat

for p being Point of (TOP-REAL n)

for A, B being Subset of (TOP-REAL n) st B is closed & p in Int A holds

for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds

h . p in Int B

for p being Point of (TOP-REAL n)

for A, B being Subset of (TOP-REAL n) st B is closed & p in Int A holds

for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds

h . p in Int B

proof end;

theorem :: BROUWER3:12

for n being Nat

for A, B being Subset of (TOP-REAL n) st A is closed & B is closed holds

for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds

( h .: (Int A) = Int B & h .: (Fr A) = Fr B )

for A, B being Subset of (TOP-REAL n) st A is closed & B is closed holds

for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds

( h .: (Int A) = Int B & h .: (Fr A) = Fr B )

proof end;

theorem Th13: :: BROUWER3:13

for n being Nat

for p being Point of (TOP-REAL n)

for r being Real st r > 0 holds

for U being Subset of (Tdisk (p,r)) st U is open & not U is empty holds

for A being Subset of (TOP-REAL n) st A = U holds

not Int A is empty

for p being Point of (TOP-REAL n)

for r being Real st r > 0 holds

for U being Subset of (Tdisk (p,r)) st U is open & not U is empty holds

for A being Subset of (TOP-REAL n) st A = U holds

not Int A is empty

proof end;

theorem :: BROUWER3:14

for n, m being Nat

for T being non empty TopSpace

for A, B being Subset of T

for r, s being Real st r > 0 & s > 0 holds

for pA being Point of (TOP-REAL n)

for pB being Point of (TOP-REAL m) st T | A, Tdisk (pA,r) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds

n = m

for T being non empty TopSpace

for A, B being Subset of T

for r, s being Real st r > 0 & s > 0 holds

for pA being Point of (TOP-REAL n)

for pB being Point of (TOP-REAL m) st T | A, Tdisk (pA,r) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds

n = m

proof end;

theorem :: BROUWER3:15

for n, m being Nat

for T being non empty TopSpace

for A, B being Subset of T

for r, s being Real st r > 0 & s > 0 holds

for pA being Point of (TOP-REAL n)

for pB being Point of (TOP-REAL m) st T | A,(TOP-REAL n) | (Ball (pA,r)) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds

n = m

for T being non empty TopSpace

for A, B being Subset of T

for r, s being Real st r > 0 & s > 0 holds

for pA being Point of (TOP-REAL n)

for pB being Point of (TOP-REAL m) st T | A,(TOP-REAL n) | (Ball (pA,r)) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds

n = m

proof end;

theorem Th15: :: BROUWER3:16

for n being Nat

for p, q being Point of (TOP-REAL n)

for r being Real holds

( (transl (p,(TOP-REAL n))) .: (Ball (q,r)) = Ball ((q + p),r) & (transl (p,(TOP-REAL n))) .: (cl_Ball (q,r)) = cl_Ball ((q + p),r) & (transl (p,(TOP-REAL n))) .: (Sphere (q,r)) = Sphere ((q + p),r) )

for p, q being Point of (TOP-REAL n)

for r being Real holds

( (transl (p,(TOP-REAL n))) .: (Ball (q,r)) = Ball ((q + p),r) & (transl (p,(TOP-REAL n))) .: (cl_Ball (q,r)) = cl_Ball ((q + p),r) & (transl (p,(TOP-REAL n))) .: (Sphere (q,r)) = Sphere ((q + p),r) )

proof end;

theorem Th16: :: BROUWER3:17

for n being Nat

for p being Point of (TOP-REAL n)

for r, s being Real st s > 0 holds

( (mlt (s,(TOP-REAL n))) .: (Ball (p,r)) = Ball ((s * p),(r * s)) & (mlt (s,(TOP-REAL n))) .: (cl_Ball (p,r)) = cl_Ball ((s * p),(r * s)) & (mlt (s,(TOP-REAL n))) .: (Sphere (p,r)) = Sphere ((s * p),(r * s)) )

for p being Point of (TOP-REAL n)

for r, s being Real st s > 0 holds

( (mlt (s,(TOP-REAL n))) .: (Ball (p,r)) = Ball ((s * p),(r * s)) & (mlt (s,(TOP-REAL n))) .: (cl_Ball (p,r)) = cl_Ball ((s * p),(r * s)) & (mlt (s,(TOP-REAL n))) .: (Sphere (p,r)) = Sphere ((s * p),(r * s)) )

proof end;

theorem Th17: :: BROUWER3:18

for n being Nat

for p being Point of (TOP-REAL n)

for r being Real

for f being additive homogeneous rotation Function of (TOP-REAL n),(TOP-REAL n) st f is onto holds

( f .: (Ball (p,r)) = Ball ((f . p),r) & f .: (cl_Ball (p,r)) = cl_Ball ((f . p),r) & f .: (Sphere (p,r)) = Sphere ((f . p),r) )

for p being Point of (TOP-REAL n)

for r being Real

for f being additive homogeneous rotation Function of (TOP-REAL n),(TOP-REAL n) st f is onto holds

( f .: (Ball (p,r)) = Ball ((f . p),r) & f .: (cl_Ball (p,r)) = cl_Ball ((f . p),r) & f .: (Sphere (p,r)) = Sphere ((f . p),r) )

proof end;

Lm4: for r being Real

for n being non zero Element of NAT

for p being Point of (TOP-REAL (n + 1)) st r <= 1 & |.p.| >= 1 & |.p.| < 1 + r & p . (n + 1) > 0 & p | n = 0* n holds

ex c being Real ex h being Function of ((TOP-REAL (n + 1)) | ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (cl_Ball (p,r)))),(Tdisk ((0. (TOP-REAL n)),c)) st

( c > 0 & h is being_homeomorphism & h .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (p,r))) = Sphere ((0. (TOP-REAL n)),c) )

proof end;

theorem :: BROUWER3:19

for n being Nat

for p, q being Point of (TOP-REAL (n + 1))

for r, s being Real st s <= r & r <= |.(p - q).| & s < |.(p - q).| & |.(p - q).| < s + r holds

ex h being Function of ((TOP-REAL (n + 1)) | ((Sphere (p,r)) /\ (cl_Ball (q,s)))),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h .: ((Sphere (p,r)) /\ (Sphere (q,s))) = Sphere ((0. (TOP-REAL n)),1) )

for p, q being Point of (TOP-REAL (n + 1))

for r, s being Real st s <= r & r <= |.(p - q).| & s < |.(p - q).| & |.(p - q).| < s + r holds

ex h being Function of ((TOP-REAL (n + 1)) | ((Sphere (p,r)) /\ (cl_Ball (q,s)))),(Tdisk ((0. (TOP-REAL n)),1)) st

( h is being_homeomorphism & h .: ((Sphere (p,r)) /\ (Sphere (q,s))) = Sphere ((0. (TOP-REAL n)),1) )

proof end;