:: Topological Manifolds :: by Karol P\kak :: :: Received June 16, 2014 :: Copyright (c) 2014-2021 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, BROUWER, CARD_1, COMPLEX1, EUCLID, FUNCT_1, METRIC_1, NAT_1, NUMBERS, ORDINAL1, PCOMPS_1, PRE_TOPC, RCOMP_1, RELAT_1, STRUCT_0, SUBSET_1, SUPINF_2, TARSKI, TOPS_1, TOPS_2, XBOOLE_0, XREAL_0, XXREAL_0, XCMPLX_0, FINSET_1, ZFMISC_1, REAL_1, SETFAM_1, T_0TOPSP, CONNSP_2, MFOLD_1, RELAT_2, EQREL_1, CONNSP_1, CONNSP_3, MFOLD_0, WAYBEL23, COMPTS_1, RLVECT_3, ORDINAL2; notations TARSKI, XBOOLE_0, FINSET_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, COMPLEX1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, XXREAL_3, NAT_1, CARD_1, REAL_1, SETFAM_1, STRUCT_0, PRE_TOPC, TOPS_1, METRIC_1, PCOMPS_1, RLVECT_1, EUCLID, TOPREAL9, TOPS_2, CONNSP_1, CONNSP_2, CONNSP_3, COMPTS_1, BROUWER, DOMAIN_1, ZFMISC_1, BORSUK_1, BORSUK_2, NAT_D, BINOP_1, EQREL_1, BORSUK_3, WAYBEL23, CANTOR_1, METRIZTS; constructors MONOID_0, CONVEX1, TOPREAL9, TOPS_1, COMPTS_1, FUNCSDOM, BROUWER, SEQ_4, EUCLID_9, SIMPLEX0, CONNSP_1, CONNSP_3, BORSUK_3, NAT_D, BORSUK_2, WAYBEL23, CANTOR_1, REAL_1, METRIZTS; registrations BORSUK_1, BROUWER, EUCLID, FUNCT_1, FUNCT_2, NAT_1, PRE_TOPC, RELAT_1, SIMPLEX2, STRUCT_0, SUBSET_1, TOPGRP_1, TOPS_1, XBOOLE_0, XREAL_0, XXREAL_0, RELSET_1, FINSET_1, TOPREALC, CARD_1, TOPREAL9, XXREAL_3, BORSUK_3, WAYBEL_2, XCMPLX_0, JORDAN1, BORSUK_2, CONNSP_1, ORDINAL1, METRIZTS, COMPTS_1, TOPREAL1; requirements ARITHM, BOOLE, NUMERALS, SUBSET, REAL; begin :: Preliminaries reserve n,m for Nat, p,q for Point of TOP-REAL n, r for Real; theorem :: MFOLD_0:1 :: MFOLD_1:1 for T being non empty TopSpace holds T , T | [#]T are_homeomorphic; definition let n,p,r; func Tball(p,r) -> SubSpace of TOP-REAL n equals :: MFOLD_0:def 1 (TOP-REAL n) | Ball(p,r); end; registration let n, p; let s be positive Real; cluster Tball(p,s) -> non empty; end; theorem :: MFOLD_0:2 :: MFOLD_1:4 the carrier of Tball(p,r) = Ball(p,r); theorem :: MFOLD_0:3 ::MFOLD_1:9 for r,s being positive Real holds Tball(p,r), Tball(q,s) are_homeomorphic; registration let n; cluster TOP-REAL n -> second-countable; end; theorem :: MFOLD_0:4 for M be non empty TopSpace for q be Point of M,r be real number,p be Point of TOP-REAL n st r>0 for U be a_neighborhood of q st M|U,Tball(p,r) are_homeomorphic ex W being a_neighborhood of q st W c= Int U & M|W,Tdisk(p,r) are_homeomorphic; begin :: Locally Euclidean Spaces reserve M,M1,M2 for non empty TopSpace; definition let M; attr M is locally_euclidean means :: MFOLD_0:def 2 for p being Point of M ex U being a_neighborhood of p, n st M|U,Tdisk(0.TOP-REAL n,1) are_homeomorphic; end; definition let n,M; attr M is n-locally_euclidean means :: MFOLD_0:def 3 for p being Point of M ex U being a_neighborhood of p st M|U,Tdisk(0.TOP-REAL n,1) are_homeomorphic; end; registration let n; cluster Tdisk(0.TOP-REAL n,1) -> n-locally_euclidean; end; registration let n; cluster n-locally_euclidean for non empty TopSpace; end; registration let n; cluster n-locally_euclidean -> locally_euclidean for non empty TopSpace; end; begin :: Locally Euclidean Spaces With and Without a Boundary definition let M be non empty TopSpace; func Int M -> Subset of M means :: MFOLD_0:def 4 for p be Point of M holds p in it iff ex U being a_neighborhood of p, n st M|U,Tball(0.TOP-REAL n,1) are_homeomorphic; end; registration let M be locally_euclidean non empty TopSpace; cluster Int M -> non empty open; end; definition let M be non empty TopSpace; func Fr M -> Subset of M equals :: MFOLD_0:def 5 (Int M)`; end; ::$N Boundary Points of Locally Euclidean Spaces theorem :: MFOLD_0:5 for M be locally_euclidean non empty TopSpace for p be Point of M holds p in Fr M iff ex U being a_neighborhood of p, n be Nat, h be Function of M|U,Tdisk(0.TOP-REAL n,1) st h is being_homeomorphism & h.p in Sphere(0.TOP-REAL n,1); begin :: Interior and Boundary of Locally Euclidean Spaces definition let M be non empty TopSpace; attr M is without_boundary means :: MFOLD_0:def 6 Int M = the carrier of M; end; notation let M be non empty TopSpace; antonym M is with_boundary for M is without_boundary; end; registration let n; cluster Tball(0.TOP-REAL n,1) -> without_boundary n-locally_euclidean; end; registration let n be non zero Nat; cluster Tdisk(0.TOP-REAL n,1) -> with_boundary; end; registration let n; cluster without_boundary for n-locally_euclidean non empty TopSpace; end; registration let n be non zero Nat; cluster with_boundary compact for n-locally_euclidean non empty TopSpace; end; registration let M be without_boundary locally_euclidean non empty TopSpace; cluster Fr M -> empty; end; registration let M be with_boundary locally_euclidean non empty TopSpace; cluster Fr M -> non empty; end; registration let n be zero Nat; cluster -> without_boundary for n-locally_euclidean non empty TopSpace; end; :: Correspondence between Classical and Extended Concepts :: of Locally Euclidean Spaces theorem :: MFOLD_0:6 M is without_boundary locally_euclidean non empty TopSpace iff for p be Point of M ex U be a_neighborhood of p,n st M|U,Tball(0.TOP-REAL n,1) are_homeomorphic; theorem :: MFOLD_0:7 for M be with_boundary locally_euclidean non empty TopSpace for p be Point of M, n st ex U be a_neighborhood of p st M|U,Tdisk(0.TOP-REAL (n+1),1) are_homeomorphic holds for pF be Point of M|Fr M st p=pF ex U being a_neighborhood of pF st (M|Fr M) |U,Tball(0.TOP-REAL n,1) are_homeomorphic; registration let M be locally_euclidean non empty TopSpace; cluster M|Int M -> locally_euclidean; cluster M|Int M -> without_boundary; end; registration let M be with_boundary locally_euclidean non empty TopSpace; cluster M|Fr M -> locally_euclidean; cluster M|Fr M -> without_boundary; end; begin :: Cartesian Product of Locally Euclidean Spaces registration let N,M be locally_euclidean non empty TopSpace; cluster [:N,M:] -> locally_euclidean; end; theorem :: MFOLD_0:8 for N,M be locally_euclidean non empty TopSpace holds Int [:N,M:] = [:Int N,Int M:]; theorem :: MFOLD_0:9 for N,M be locally_euclidean non empty TopSpace holds Fr [:N,M:] = [:[#]N,Fr M:] \/ [:Fr N,[#]M:]; registration let N,M be without_boundary locally_euclidean non empty TopSpace; cluster [:N,M:] -> without_boundary; end; registration let N be locally_euclidean non empty TopSpace; let M be with_boundary locally_euclidean non empty TopSpace; cluster [:N,M:] -> with_boundary; cluster [:M,N:] -> with_boundary; end; begin :: Fixed Dimension Locally Euclidean Spaces definition let n; let M be n-locally_euclidean non empty TopSpace; redefine func Int M -> Subset of M means :: MFOLD_0:def 7 for p be Point of M holds p in it iff ex U being a_neighborhood of p st M|U,Tball(0.TOP-REAL n,1) are_homeomorphic; end; definition let n; let M be n-locally_euclidean non empty TopSpace; redefine func Fr M -> Subset of M means :: MFOLD_0:def 8 for p be Point of M holds p in it iff ex U being a_neighborhood of p, h be Function of M|U,Tdisk(0.TOP-REAL n,1) st h is being_homeomorphism & h.p in Sphere(0.TOP-REAL n,1); end; theorem :: MFOLD_0:10 M1 is locally_euclidean & M1,M2 are_homeomorphic implies M2 is locally_euclidean; theorem :: MFOLD_0:11 M1 is n-locally_euclidean & M2 is locally_euclidean & M1,M2 are_homeomorphic implies M2 is n-locally_euclidean; ::$N Topological Invariance of Dimension of Locally Euclidean Spaces theorem :: MFOLD_0:12 M is n-locally_euclidean & M is m-locally_euclidean implies n = m; theorem :: MFOLD_0:13 M is without_boundary n-locally_euclidean non empty TopSpace iff for p be Point of M ex U be a_neighborhood of p st M|U,Tball(0.TOP-REAL n,1) are_homeomorphic; ::$N Dimension of the Cartesian Product of Locally Euclidean Spaces registration let n,m be Element of NAT; let N be n-locally_euclidean non empty TopSpace; let M be m-locally_euclidean non empty TopSpace; cluster [:N,M:] -> (n+m)-locally_euclidean; end; ::$N Dimension of the Interior of Locally Euclidean Spaces registration let n; let M be n-locally_euclidean non empty TopSpace; cluster M|Int M -> n-locally_euclidean for non empty TopSpace; end; ::$N Dimension of the Boundary of Locally Euclidean Spaces registration let n be non zero Nat; let M be with_boundary n-locally_euclidean non empty TopSpace; cluster M|Fr M -> (n-'1)-locally_euclidean for non empty TopSpace; end; begin :: Connected Components of Locally Euclidean Spaces theorem :: MFOLD_0:14 for M be compact locally_euclidean non empty TopSpace for C be Subset of M st C is a_component holds C is open & ex n st M|C is n-locally_euclidean non empty TopSpace; theorem :: MFOLD_0:15 for M be compact locally_euclidean non empty TopSpace ex P be a_partition of the carrier of M st for A be Subset of M st A in P holds A is open a_component & ex n st M|A is n-locally_euclidean non empty TopSpace; theorem :: MFOLD_0:16 for M be compact locally_euclidean non empty TopSpace st M is connected ex n st M is n-locally_euclidean; begin :: Topological Manifold registration let n; cluster second-countable Hausdorff n-locally_euclidean for non empty TopSpace; end; definition mode topological_manifold is second-countable Hausdorff locally_euclidean non empty TopSpace; end; notation let n; let M be topological_manifold; synonym M is n-dimensional for M is n-locally_euclidean; end; registration let n; cluster n-dimensional without_boundary for topological_manifold; end; registration let n be non zero Nat; cluster n-dimensional compact with_boundary for topological_manifold; end; registration let M be topological_manifold; cluster -> second-countable Hausdorff for non empty SubSpace of M; end; registration let M1,M2 be topological_manifold; cluster [:M1,M2:] -> second-countable Hausdorff; end;