:: Brouwer Invariance of Domain Theorem
:: by Karol P\kak
::
:: Received February 11, 2014
:: Copyright (c) 2014-2021 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;

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

coherence
for b₁ being Function of X,(TOP-REAL n) holds b₁ is FinSequence-yielding

proof end;

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

proof end;

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

cluster f ^^ g -> continuous for Function of T,(TOP-REAL (n + m));

coherence
for b₁ being Function of T,(TOP-REAL (n + m)) st b₁ = f ^^ g holds
b₁ is continuous

proof end;

end;

definition

let f be real-valued Function;

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
ex b₁ being Function st
( dom b₁ = dom f & ( for x being object st x in dom b₁ holds
b₁ . x = |[(f . x)]| ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = dom f & ( for x being object st x in dom b₁ holds
b₁ . x = |[(f . x)]| ) & dom b₂ = dom f & ( for x being object st x in dom b₂ holds
b₂ . x = |[(f . x)]| ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines |[ BROUWER3:def 1 :
for f being real-valued Function
for b₂ being Function holds
( b₂ = |[f]| iff ( dom b₂ = dom f & ( for x being object st x in dom b₂ holds
b₂ . x = |[(f . x)]| ) ) );

registration

let f be real-valued Function;

cluster |[f]| -> the carrier of (TOP-REAL 1) -valued ;

coherence
|[f]| is the carrier of (TOP-REAL 1) -valued

proof end;

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)

proof end;

end;

registration

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

cluster |[f]| -> continuous for Function of T,(TOP-REAL 1);

coherence
for b₁ being Function of T,(TOP-REAL 1) st b₁ = |[f]| holds
b₁ is continuous

proof end;

end;

registration

let T be non empty TopSpace;
let f be continuous RealMap of T;

cluster |[f]| -> continuous for Function of T,(TOP-REAL 1);

coherence
for b₁ being Function of T,(TOP-REAL 1) st b₁ = |[f]| holds
b₁ is continuous

proof end;

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

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 )

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

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

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)

proof end;

theorem Th6: :: BROUWER3:6

for n being Nat
for A being Subset of (TOP-REAL n) st not A is boundary holds
ind A = n

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

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

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

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

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

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 )

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

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

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

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

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

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

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

proof end;