BROUWER3: Brouwer Invariance of Domain Theorem

:: Brouwer Invariance of Domain Theorem
:: by Karol P\kak
::
:: Received February 11, 2014
:: Copyright (c) 2014-2016 Association of Mizar Users

environ

vocabularies HIDDEN, ARYTM_1, ARYTM_3, BROUWER, CARD_1, COMPLEX1, CONVEX1, EUCLID, FUNCOP_1, FUNCT_1, FUNCT_4, JGRAPH_4, MEMBERED, METRIC_1, NAT_1, NUMBERS, ORDINAL2, PCOMPS_1, PRE_TOPC, RCOMP_1, REAL_1, RELAT_1, STRUCT_0, SUBSET_1, SUPINF_2, TARSKI, TOPMETR, TOPS_1, TOPS_2, VALUED_1, XBOOLE_0, XXREAL_0, FUNCT_2, EUCLID_9, TOPREALC, FINSEQ_1, FINSEQ_2, CARD_3, PARTFUN3, SQUARE_1, XCMPLX_0, PARTFUN1, FINSET_1, VALUED_0, ORDINAL4, PRE_POLY, PSCOMP_1, RVSUM_1, VALUED_2, T_0TOPSP, WAYBEL23, TOPDIM_1, MATRTOP3, TOPREALB, RLTOPSP1, FUNCT_3, RLAFFIN1, RLVECT_5, MEASURE5, BORSUK_1, UNIALG_1, MSSUBFAM, MATRLIN, MESFUNC1, VECTSP_1;
notations HIDDEN, TARSKI, XBOOLE_0, FINSET_1, VALUED_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, COMPLEX1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, RVSUM_1, VALUED_1, VALUED_2, XXREAL_3, XCMPLX_0, NAT_1, CARD_1, MEMBERED, FUNCOP_1, FINSEQ_1, FINSEQ_2, STRUCT_0, PRE_TOPC, TOPS_1, PSCOMP_1, METRIC_1, PCOMPS_1, TOPMETR, FUNCT_7, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL9, PARTFUN3, TOPS_2, COMPTS_1, TBSP_1, JGRAPH_4, TMAP_1, BROUWER, EUCLID_9, CARD_3, SQUARE_1, PRE_POLY, JORDAN2B, WAYBEL23, T_0TOPSP, METRIZTS, RLAFFIN1, TOPREALB, FUNCT_4, DOMAIN_1, CONVEX1, TIETZE_2, RLVECT_5, BORSUK_1, VECTSP_1, TOPREALC, MATRTOP3, MATRIX_1, TOPDIM_1;
definitions TARSKI, XBOOLE_0;
theorems ABSVALUE, BORSUK_1, BROUWER, COMPLEX1, EUCLID, FUNCOP_1, FUNCT_1, FUNCT_2, FUNCT_4, GOBOARD6, JGRAPH_4, JORDAN24, NECKLACE, ORDINAL1, PRE_TOPC, RELAT_1, RLAFFIN1, RLAFFIN3, RLTOPSP1, RLVECT_1, SIMPLEX2, SUBSET_1, TARSKI, TBSP_1, TMAP_1, TOPMETR, TOPREAL9, TOPREALB, TOPREALC, TOPRNS_1, TOPS_1, TOPS_2, VALUED_2, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_0, XREAL_1, XXREAL_0, ZFMISC_1, EUCLID_9, FINSEQ_2, CARD_1, FINSEQ_1, PARTFUN3, YELLOW_8, FINSEQ_3, RVSUM_1, VALUED_1, PARTFUN1, FUNCT_7, TOPREAL7, TSEP_1, BROUWER2, NAT_1, REAL_NS1, SQUARE_1, TOPGRP_1, PRE_POLY, JORDAN2B, FINSEQ_4, JORDAN5A, VECTSP_1, JORDAN, ENUMSET1, TOPDIM_1, TOPDIM_2, MATRTOP3, TOPGEN_5, METRIZTS, T_0TOPSP, TIETZE_2;
schemes FINSEQ_1, FUNCT_2, FUNCT_1, NAT_1;
registrations BORSUK_1, BROUWER, EUCLID, EUCLID_9, FUNCOP_1, FINSEQ_1, FUNCT_1, FUNCT_2, JGRAPH_4, MEMBERED, NAT_1, PCOMPS_1, PRE_TOPC, RELAT_1, PARTFUN3, RVSUM_1, SIMPLEX2, STRUCT_0, SUBSET_1, TMAP_1, TOPGRP_1, TOPMETR, TOPS_1, VALUED_0, VALUED_2, XBOOLE_0, XREAL_0, XXREAL_0, RELSET_1, FINSET_1, MONOID_0, SQUARE_1, FUNCT_7, NUMBERS, JORDAN2B, FINSEQ_2, TOPREALC, PARTFUN4, COMPTS_1, TOPREALB, CARD_1, INT_1, TOPREAL1, TOPREAL9, METRIZTS, RLTOPSP1, RLAFFIN1, RLAFFIN3, XXREAL_3, TOPDIM_1, TOPDIM_2, REVROT_1, WAYBEL_2, XCMPLX_0, ZFMISC_1, VECTSP_1, PRE_POLY, VALUED_1, MATRTOP3;
constructors HIDDEN, TBSP_1, MONOID_0, CONVEX1, TOPS_1, COMPTS_1, FUNCSDOM, PARTFUN3, JGRAPH_4, TMAP_1, TOPREALC, BROUWER, EUCLID_9, SQUARE_1, JORDAN2B, PSCOMP_1, WAYBEL23, TOPDIM_1, METRIZTS, SIMPLEX0, RLAFFIN1, BORSUK_3, RLVECT_5, MATRTOP3, TIETZE_2, LAPLACE;
requirements HIDDEN, ARITHM, BOOLE, NUMERALS, SUBSET, REAL;
equalities FUNCOP_1, STRUCT_0, SQUARE_1, XCMPLX_0, ALGSTR_0, TOPREAL9, BROUWER, FINSEQ_1, ORDINAL1, EUCLID, FINSEQ_2;
expansions TARSKI, FUNCT_1, XBOOLE_0, FINSEQ_1;

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

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

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

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

proof end;

uniqueness

proof end;

end;

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

registration

let f be real-valued Function;

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

coherence

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

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

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

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;