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