:: Brouwer Invariance of Domain Theorem
:: by Karol P\kak
::
:: Copyright (c) 2014-2021 Association of Mizar Users

Lm1: for n being Nat
for V being Subset of () st V is open holds
for e being Point of () 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 ()
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 ()));
coherence
for b1 being Function of X,() holds b1 is FinSequence-yielding
proof end;
end;

definition
let X be set ;
let n, m be Nat;
let f be Function of X,();
let g be Function of X,();
:: 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,();
let g be continuous Function of T,();
cluster f ^^ g -> continuous for Function of T,(TOP-REAL (n + m));
coherence
for b1 being Function of T,(TOP-REAL (n + m)) st b1 = f ^^ g holds
b1 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 b1 being Function st
( dom b1 = dom f & ( for x being object st x in dom b1 holds
b1 . x = |[(f . x)]| ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = dom f & ( for x being object st x in dom b1 holds
b1 . x = |[(f . x)]| ) & dom b2 = dom f & ( for x being object st x in dom b2 holds
b2 . x = |[(f . x)]| ) holds
b1 = b2
proof end;
end;

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

registration
let f be real-valued Function;
cluster |[f]| -> the carrier of () -valued ;
coherence
|[f]| is the carrier of () -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,();
coherence
|[f]| is Function of X,()
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,();
coherence
for b1 being Function of T,() st b1 = |[f]| holds
b1 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,();
coherence
for b1 being Function of T,() st b1 = |[f]| holds
b1 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. ()),1) & <:F:> .: Sn = cl_Ball ((0. ()),1) & <:F:> .: (Sp /\ Sn) = Sphere ((0. ()),1) & ( for H being Function of ((TOP-REAL (N + 1)) | Sp),(Tdisk ((0. ()),1)) st H = <:F:> | Sp holds
H is being_homeomorphism ) & ( for H being Function of ((TOP-REAL (N + 1)) | Sn),(Tdisk ((0. ()),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 () st Sp = { s where s is Point of () : ( s . n >= 0 & |.s.| = 1 ) } & Sn = { t where t is Point of () : ( 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 ()
for A being Subset of ()
for r being Real st not p in A & r > 0 holds
ex h being Function of (() | A),(() | (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 ()
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 () 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 ()
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 ()
for p being Point of () st n > 0 & p in A & ( for r being Real st r > 0 holds
ex U being open Subset of (() | A) st
( p in U & U c= Ball (p,r) & ( for f being Function of (() | (A \ U)),() st f is continuous holds
ex h being Function of (() | A),() 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 ()
for p being Point of () st p in Fr A & A is closed holds
for r being Real st r > 0 holds
ex U being open Subset of (() | A) st
( p in U & U c= Ball (p,r) & ( for f being Function of (() | (A \ U)),() st f is continuous holds
ex h being Function of (() | A),() st
( h is continuous & h | (A \ U) = f ) ) )
proof end;

Lm3: for n being Nat
for A, B being Subset of () st n = 0 holds
for h being Function of (() | A),(() | B) st h is being_homeomorphism holds
for p being Point of () 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 ()
for A, B being Subset of () st A is closed & p in Fr A holds
for h being Function of (() | A),(() | 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 ()
for A, B being Subset of () st B is closed & p in Int A holds
for h being Function of (() | A),(() | 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 () st A is closed & B is closed holds
for h being Function of (() | A),(() | 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 ()
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 () 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 ()
for pB being Point of () 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 ()
for pB being Point of () st T | A,() | (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 ()
for r being Real holds
( (transl (p,())) .: (Ball (q,r)) = Ball ((q + p),r) & (transl (p,())) .: (cl_Ball (q,r)) = cl_Ball ((q + p),r) & (transl (p,())) .: (Sphere (q,r)) = Sphere ((q + p),r) )
proof end;

theorem Th16: :: BROUWER3:17
for n being Nat
for p being Point of ()
for r, s being Real st s > 0 holds
( (mlt (s,())) .: (Ball (p,r)) = Ball ((s * p),(r * s)) & (mlt (s,())) .: (cl_Ball (p,r)) = cl_Ball ((s * p),(r * s)) & (mlt (s,())) .: (Sphere (p,r)) = Sphere ((s * p),(r * s)) )
proof end;

theorem Th17: :: BROUWER3:18
for n being Nat
for p being Point of ()
for r being Real
for f being additive homogeneous rotation Function of (),() 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. ()),c)) st
( c > 0 & h is being_homeomorphism & h .: ((Sphere ((0. (TOP-REAL (n + 1))),1)) /\ (Sphere (p,r))) = Sphere ((0. ()),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. ()),1)) st
( h is being_homeomorphism & h .: ((Sphere (p,r)) /\ (Sphere (q,s))) = Sphere ((0. ()),1) )
proof end;