:: Tietze Extension Theorem for $n$-dimensional Spaces
:: by Karol P\kak
::
:: Received February 11, 2014
:: Copyright (c) 2014-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ARYTM_1, ARYTM_3, CARD_1, COMPLEX1, CONVEX1, EUCLID, FUNCOP_1,
FUNCT_1, FUNCT_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, XBOOLE_0, XREAL_0, XXREAL_0, XXREAL_2, FUNCT_2,
EUCLID_9, TOPREALC, FINSEQ_1, XXREAL_1, FINSEQ_2, CARD_3, PARTFUN3,
SQUARE_1, FUNCT_6, XCMPLX_0, PARTFUN1, FINSET_1, ZFMISC_1, VALUED_0,
SETFAM_1, T_0TOPSP, BROUWER, ORDINAL4, TIETZE_2, FUNCT_3;
notations TARSKI, XBOOLE_0, FINSET_1, SETFAM_1, VALUED_0, SUBSET_1, RELAT_1,
FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, COMPLEX1, ORDINAL1, NUMBERS,
XXREAL_0, XREAL_0, RVSUM_1, XCMPLX_0, MEMBERED, FUNCOP_1, FINSEQ_1,
FINSEQ_2, STRUCT_0, PRE_TOPC, TOPS_1, METRIC_1, PCOMPS_1, TOPMETR,
FUNCT_7, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL9, PARTFUN3, TOPS_2,
COMPTS_1, TBSP_1, XXREAL_2, EUCLID_9, CARD_3, SQUARE_1, FUNCT_6,
TOPREALC, METRIZTS, ZFMISC_1, RCOMP_1, BORSUK_1, T_0TOPSP, BINOP_1,
FUNCT_3, NAT_1, BORSUK_2, BROUWER, TMAP_1;
constructors COMPLEX1, TBSP_1, MONOID_0, CONVEX1, TOPREAL9, TOPS_1, COMPTS_1,
FUNCSDOM, PARTFUN3, TOPREALC, SEQ_4, EUCLID_9, SQUARE_1, FUNCT_6,
METRIZTS, BORSUK_3, BORSUK_2, BROUWER, TMAP_1;
registrations BORSUK_1, EUCLID, EUCLID_9, FUNCOP_1, FINSEQ_1, FUNCT_1,
FUNCT_2, MEMBERED, NAT_1, PCOMPS_1, PRE_TOPC, RELAT_1, PARTFUN3, RVSUM_1,
SIMPLEX2, STRUCT_0, SUBSET_1, TOPGRP_1, TOPMETR, TOPS_1, VALUED_0,
VALUED_2, XBOOLE_0, XREAL_0, XXREAL_0, RELSET_1, FINSET_1, TBSP_1,
MONOID_0, JORDAN2B, FINSEQ_2, XXREAL_2, COMPTS_1, CARD_1, TOPREAL1,
RLAFFIN3, XCMPLX_0, TOPREAL9, FUNCT_3, FUNCT_6, NUMBERS, BORSUK_2,
TMAP_1, TOPREALC;
requirements ARITHM, BOOLE, NUMERALS, SUBSET, REAL;
begin :: Closed Hypercube
reserve n,m,i for Nat,
p,q for Point of TOP-REAL n,
r,s for Real,
R for real-valued FinSequence;
registration
cluster empty -> nonnegative-yielding for FinSequence;
end;
definition
let n be non zero Nat;
let X be set;
let F be Element of n-tuples_on Funcs(X,the carrier of R^1);
redefine func <:F:> -> Function of X,TOP-REAL n;
end;
theorem :: TIETZE_2:1
for X,Y be set for F be Function-yielding Function
for x,y be object st F is Funcs(X,Y)-valued or y in dom <:F:>
holds F.x.y = <:F:>.y.x;
definition
let n,p,r;
func OpenHypercube(p,r) -> open Subset of TOP-REAL n means
:: TIETZE_2:def 1
ex e be Point of Euclid n st p=e & it = OpenHypercube(e,r);
end;
theorem :: TIETZE_2:2
q in OpenHypercube(p,r) & s in ].p.i - r, p.i + r.[
implies q+*(i,s) in OpenHypercube(p,r);
theorem :: TIETZE_2:3
i in Seg n implies PROJ(n,i).:OpenHypercube(p,r) = ]. p.i - r, p.i + r .[;
theorem :: TIETZE_2:4
q in OpenHypercube(p,r)
iff
for i st i in Seg n holds q.i in ]. p.i - r,p.i +r .[;
definition
let n,p,R;
func ClosedHypercube(p,R) -> Subset of TOP-REAL n means
:: TIETZE_2:def 2
q in it iff for i st i in Seg n holds q.i in [. p.i - R.i,p.i+R.i .];
end;
theorem :: TIETZE_2:5
(ex i st i in Seg n /\ dom R & R.i < 0) implies ClosedHypercube(p,R) is empty
;
theorem :: TIETZE_2:6
(for i st i in Seg n /\ dom R holds R.i >= 0)
implies p in ClosedHypercube(p,R);
registration
let n,p;
let R be nonnegative-yielding real-valued FinSequence;
cluster ClosedHypercube(p,R) -> non empty;
end;
registration
let n,p,R;
cluster ClosedHypercube(p,R) -> convex compact;
end;
theorem :: TIETZE_2:7
i in Seg n & q in ClosedHypercube(p,R) & r in [.p.i - R.i, p.i + R.i.]
implies q+*(i,r) in ClosedHypercube(p,R);
theorem :: TIETZE_2:8
i in Seg n & ClosedHypercube(p,R) is non empty implies
PROJ(n,i).:ClosedHypercube(p,R) = [. p.i - R.i, p.i + R.i .];
theorem :: TIETZE_2:9
n <= len R & r <= inf (rng R) implies
OpenHypercube(p,r) c= ClosedHypercube(p,R);
theorem :: TIETZE_2:10
q in Fr ClosedHypercube(p,R)
iff
q in ClosedHypercube(p,R) & ex i st i in Seg n &
(q.i = p.i - R.i or q.i = p.i + R. i);
theorem :: TIETZE_2:11
r >= 0 implies p in ClosedHypercube(p,n|->r);
theorem :: TIETZE_2:12
r>0 implies Int ClosedHypercube(p,n|->r) = OpenHypercube(p,r);
theorem :: TIETZE_2:13
OpenHypercube(p,r) c= ClosedHypercube(p,n|->r);
theorem :: TIETZE_2:14
r < s implies ClosedHypercube(p,n|->r) c= OpenHypercube(p,s);
registration
let n,p;
let r be positive Real;
cluster ClosedHypercube(p,n|->r) -> non boundary;
end;
begin :: Properties of the Product of Closed Hypercube
reserve T1,T2,S1,S2 for non empty TopSpace,
t1 for Point of T1, t2 for Point of T2,
pn,qn for Point of TOP-REAL n,
pm,qm for Point of TOP-REAL m;
theorem :: TIETZE_2:15
for f be Function of T1,T2 for g be Function of S1,S2 st
f is being_homeomorphism & g is being_homeomorphism holds
[:f,g:] is being_homeomorphism;
theorem :: TIETZE_2:16
for r,s st r>0 & s>0
ex h be Function of
[: (TOP-REAL n)|ClosedHypercube(pn,n|->r),
(TOP-REAL m)|ClosedHypercube(pm,m|->s):],
(TOP-REAL (n+m))|ClosedHypercube(0.TOP-REAL (n+m),(n+m)|->1) st
h is being_homeomorphism &
h.:[: OpenHypercube(pn,r),OpenHypercube(pm,s):]
= OpenHypercube(0.TOP-REAL (n+m),1);
theorem :: TIETZE_2:17
for r,s st r>0 & s>0
for f be Function of T1,(TOP-REAL n)|ClosedHypercube(pn,n|->r)
for g be Function of T2,(TOP-REAL m)| ClosedHypercube(pm,m|->s)
st f is being_homeomorphism & g is being_homeomorphism
holds
ex h be Function of [:T1,T2:],(TOP-REAL (n+m))|
ClosedHypercube(0.TOP-REAL (n+m),(n+m)|->1)
st h is being_homeomorphism &
for t1, t2 holds
f.t1 in OpenHypercube(pn,r) & g.t2 in OpenHypercube(pm,s)
iff
h. (t1,t2) in OpenHypercube(0.TOP-REAL (n+m),1);
registration
let n;
cluster non boundary convex compact for Subset of TOP-REAL n;
end;
theorem :: TIETZE_2:18
for A be non boundary convex compact Subset of TOP-REAL n,
B be non boundary convex compact Subset of TOP-REAL m,
C be non boundary convex compact Subset of TOP-REAL (n+m)
for f be Function of T1,(TOP-REAL n)| A,
g be Function of T2,(TOP-REAL m)| B
st f is being_homeomorphism & g is being_homeomorphism
holds
ex h be Function of [:T1,T2:],(TOP-REAL (n+m))| C
st h is being_homeomorphism &
for t1, t2 holds f.t1 in Int A & g.t2 in Int B
iff
h.(t1,t2) in Int C;
theorem :: TIETZE_2:19
for pn be Point of TOP-REAL n,pm be Point of TOP-REAL m
for r,s st r>0 & s>0
ex h be Function of [: Tdisk(pn,r),Tdisk(pm,s):],Tdisk(0.TOP-REAL (n+m),1)
st h is being_homeomorphism &
h.:[:Ball(pn,r), Ball(pm,s):] = Ball(0.TOP-REAL (n+m),1);
theorem :: TIETZE_2:20
r >0 & s>0 &
T1,(TOP-REAL n)|Ball(pn,r) are_homeomorphic &
T2,(TOP-REAL m)|Ball(pm,s) are_homeomorphic
implies
[:T1,T2:],(TOP-REAL (n+m))|Ball(0.TOP-REAL (n+m),1) are_homeomorphic;
begin :: Tietze Extension Theorem
reserve T,S for TopSpace,
A for closed Subset of T,
B for Subset of S;
theorem :: TIETZE_2:21
for n be non zero Nat
for F be Element of n-tuples_on Funcs(the carrier of T,the carrier of R^1)
st for i st i in dom F for h be Function of T,R^1 st h = F.i
holds h is continuous holds <:F:> is continuous;
theorem :: TIETZE_2:22
for T,A st T is normal
for f being Function of (T | A),
(TOP-REAL n) | ClosedHypercube(0.TOP-REAL n,n|->1)
st f is continuous
ex g being Function of T,
(TOP-REAL n) | ClosedHypercube(0.TOP-REAL n,n|->1)
st g is continuous & g|A = f;
theorem :: TIETZE_2:23
for T,A st T is normal
for X be Subset of TOP-REAL n st X is compact non boundary convex
for f being Function of T|A,(TOP-REAL n) | X st
f is continuous
ex g being Function of T,(TOP-REAL n) | X st g is continuous & g|A=f;
::$N Tietze Extension Theorem for n-dimensional spaces
::$N The First Implication
theorem :: TIETZE_2:24
for T,S,A,B st T is normal
for X be Subset of TOP-REAL n st
X is compact non boundary convex & B,X are_homeomorphic
for f being Function of T|A,S|B st f is continuous
ex g being Function of T,S|B st g is continuous & g|A = f;
::$N The Second Implication
theorem :: TIETZE_2:25
for T be non empty TopSpace, n st n>=1 &
for S be TopSpace,A be non empty closed Subset of T,B being Subset of S
st ex X be Subset of TOP-REAL n st
X is compact non boundary convex & B,X are_homeomorphic
holds
for f being Function of T|A,S|B st f is continuous
ex g being Function of T,S|B st g is continuous & g|A = f
holds T is normal;