Home Metamath Proof ExplorerTheorem List (p. 248 of 322) < Previous  Next > Browser slow? Try the Unicode version.

 Color key: Metamath Proof Explorer (1-22262) Hilbert Space Explorer (22263-23785) Users' Mathboxes (23786-32130)

Theorem List for Metamath Proof Explorer - 24701-24800   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremcvxpcon 24701* A convex subset of the complex numbers is path-connected. (Contributed by Mario Carneiro, 12-Feb-2015.)
fld       t        PCon

Theoremcvxscon 24702* A convex subset of the complex numbers is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015.)
fld       t        SCon

Theoremblscon 24703 An open ball in the complex numbers is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015.)
fld              t        SCon

Theoremcnllyscon 24704 The topology of the complex numbers is locally simply connected. (Contributed by Mario Carneiro, 2-Mar-2015.)
fld       Locally SCon

Theoremrescon 24705 A subset of is simply connected iff it is connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
t        SCon

Theoremiooscon 24706 An open interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
t SCon

Theoremiccscon 24707 A closed interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
t SCon

Theoremretopscon 24708 The real numbers are simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
SCon

Theoremiccllyscon 24709 A closed interval is locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.)
t Locally SCon

Theoremrellyscon 24710 The real numbers are locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.)
Locally SCon

Theoremiiscon 24711 The unit interval is simply connected. (Contributed by Mario Carneiro, 9-Mar-2015.)
SCon

Theoremiillyscon 24712 The unit interval is locally simply connected. (Contributed by Mario Carneiro, 10-Mar-2015.)
Locally SCon

Theoremiinllycon 24713 The unit interval is locally connected. (Contributed by Mario Carneiro, 6-Jul-2015.)
𝑛Locally

19.4.9  Covering maps

Syntaxccvm 24714 Extend class notation with the class of covering maps.
CovMap

Definitiondf-cvm 24715* Define the class of covering maps on two topological spaces. A function is a covering map if it is continuous and for every point in the target space there is a neighborhood of and a decomposition of the preimage of as a disjoint union such that is a homeomorphism of each set onto . (Contributed by Mario Carneiro, 13-Feb-2015.)
CovMap t t

Theoremfncvm 24716 Lemma for covering maps. (Contributed by Mario Carneiro, 13-Feb-2015.)
CovMap

Theoremcvmscbv 24717* Change bound variables in the set of even coverings. (Contributed by Mario Carneiro, 17-Feb-2015.)
t t        t t

Theoremiscvm 24718* The property of being a covering map. (Contributed by Mario Carneiro, 13-Feb-2015.)
t t               CovMap

Theoremcvmtop1 24719 Reverse closure for a covering map. (Contributed by Mario Carneiro, 11-Feb-2015.)
CovMap

Theoremcvmtop2 24720 Reverse closure for a covering map. (Contributed by Mario Carneiro, 13-Feb-2015.)
CovMap

Theoremcvmcn 24721 A covering map is a continuous function. (Contributed by Mario Carneiro, 13-Feb-2015.)
CovMap

Theoremcvmcov 24722* Property of a covering map. In order to make the covering property more manageable, we define here the set of all even coverings of an open set in the range. Then the covering property states that every point has a neighborhood which has an even covering. (Contributed by Mario Carneiro, 13-Feb-2015.)
t t               CovMap

Theoremcvmsrcl 24723* Reverse closure for an even covering. (Contributed by Mario Carneiro, 11-Feb-2015.)
t t

Theoremcvmsi 24724* One direction of cvmsval 24725. (Contributed by Mario Carneiro, 13-Feb-2015.)
t t        t t

Theoremcvmsval 24725* Elementhood in the set of all even coverings of an open set in . is an even covering of if it is a nonempty collection of disjoint open sets in whose union is the preimage of , such that each set is homeomorphic under to . (Contributed by Mario Carneiro, 13-Feb-2015.)
t t        t t

Theoremcvmsss 24726* An even covering is a subset of the topology of the domain (i.e. a collection of open sets). (Contributed by Mario Carneiro, 11-Feb-2015.)
t t

Theoremcvmsn0 24727* An even covering is nonempty. (Contributed by Mario Carneiro, 11-Feb-2015.)
t t

Theoremcvmsuni 24728* An even covering of has union equal to the preimage of by . (Contributed by Mario Carneiro, 11-Feb-2015.)
t t

Theoremcvmsdisj 24729* An even covering of is a disjoint union. (Contributed by Mario Carneiro, 13-Feb-2015.)
t t

Theoremcvmshmeo 24730* Every element of an even covering of is homeomorphic to via . (Contributed by Mario Carneiro, 13-Feb-2015.)
t t        t t

Theoremcvmsf1o 24731* , localized to an element of an even covering of , is a bijection. (Contributed by Mario Carneiro, 14-Feb-2015.)
t t        CovMap

Theoremcvmscld 24732* The sets of an even covering are clopen in the subspace topology on . (Contributed by Mario Carneiro, 14-Feb-2015.)
t t        CovMap t

Theoremcvmsss2 24733* An open subset of an evenly covered set is evenly covered. (Contributed by Mario Carneiro, 7-Jul-2015.)
t t        CovMap

Theoremcvmcov2 24734* The covering map property can be restricted to an open subset. (Contributed by Mario Carneiro, 7-Jul-2015.)
t t        CovMap

Theoremcvmseu 24735* Every element in is a member of a unique element of . (Contributed by Mario Carneiro, 14-Feb-2015.)
t t               CovMap

Theoremcvmsiota 24736* Identify the unique element of containing . (Contributed by Mario Carneiro, 14-Feb-2015.)
t t                      CovMap

Theoremcvmopnlem 24737* Lemma for cvmopn 24739. (Contributed by Mario Carneiro, 7-May-2015.)
t t               CovMap

Theoremcvmfolem 24738* Lemma for cvmfo 24759. (Contributed by Mario Carneiro, 13-Feb-2015.)
t t                      CovMap

Theoremcvmopn 24739 A covering map is an open map. (Contributed by Mario Carneiro, 7-May-2015.)
CovMap

Theoremcvmliftmolem1 24740* Lemma for cvmliftmo 24743. (Contributed by Mario Carneiro, 10-Mar-2015.)
CovMap               𝑛Locally                                           t t                             t

Theoremcvmliftmolem2 24741* Lemma for cvmliftmo 24743. (Contributed by Mario Carneiro, 10-Mar-2015.)
CovMap               𝑛Locally                                           t t

Theoremcvmliftmoi 24742 A lift of a continuous function from a connected and locally connected space over a covering map is unique when it exists. (Contributed by Mario Carneiro, 10-Mar-2015.)
CovMap               𝑛Locally

Theoremcvmliftmo 24743* A lift of a continuous function from a connected and locally connected space over a covering map is unique when it exists. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by NM, 17-Jun-2017.)
CovMap               𝑛Locally

Theoremcvmliftlem1 24744* Lemma for cvmlift 24758. In cvmliftlem15 24757, we picked an large enough so that the sections are all contained in an even covering, and the function enumerates these even coverings. So is a neighborhood of , and is an even covering of , which is to say a disjoint union of open sets in whose image is . (Contributed by Mario Carneiro, 14-Feb-2015.)
t t                      CovMap

Theoremcvmliftlem2 24745* Lemma for cvmlift 24758. is a subset of for each . (Contributed by Mario Carneiro, 16-Feb-2015.)
t t                      CovMap

Theoremcvmliftlem3 24746* Lemma for cvmlift 24758. Since is a neighborhood of , every element satisfies . (Contributed by Mario Carneiro, 16-Feb-2015.)
t t                      CovMap

Theoremcvmliftlem4 24747* Lemma for cvmlift 24758. The function will be our lifted path, defined piecewise on each section for . For , it is a "seed" value which makes the rest of the recursion work, a singleton function mapping to . (Contributed by Mario Carneiro, 15-Feb-2015.)
t t                      CovMap

Theoremcvmliftlem5 24748* Lemma for cvmlift 24758. Definition of at a successor. This is a function defined on as where is the unique covering set of that contains evaluated at the last defined point, namely (note that for this is using the seed value ). (Contributed by Mario Carneiro, 15-Feb-2015.)
t t                      CovMap

Theoremcvmliftlem6 24749* Lemma for cvmlift 24758. Induction step for cvmliftlem7 24750. Assuming that is defined at and is a preimage of , the next segment is also defined and is a function on which is a lift for this segment. This follows explicitly from the definition since is in for the entire interval so that maps this into and maps back to . (Contributed by Mario Carneiro, 16-Feb-2015.)
t t                      CovMap

Theoremcvmliftlem7 24750* Lemma for cvmlift 24758. Prove by induction that every function is well-defined (we can immediately follow this theorem with cvmliftlem6 24749 to show functionality and lifting of ). (Contributed by Mario Carneiro, 14-Feb-2015.)
t t                      CovMap

Theoremcvmliftlem8 24751* Lemma for cvmlift 24758. The functions are continuous functions because they are defined as where is continuous and is a homeomorphism. (Contributed by Mario Carneiro, 16-Feb-2015.)
t t                      CovMap                                                                       t

Theoremcvmliftlem9 24752* Lemma for cvmlift 24758. The functions are defined on almost disjoint intervals, but they overlap at the edges. Here we show that at these points the functions agree on their common domain. (Contributed by Mario Carneiro, 14-Feb-2015.)
t t                      CovMap

Theoremcvmliftlem10 24753* Lemma for cvmlift 24758. The function is going to be our complete lifted path, formed by unioning together all the functions (each of which is defined on one segment of the interval). Here we prove by induction that is a continuous function and a lift of by applying cvmliftlem6 24749, cvmliftlem7 24750 (to show it is a function and a lift), cvmliftlem8 24751 (to show it is continuous), and cvmliftlem9 24752 (to show that different functions agree on the intersection of their domains, so that the pasting lemma paste 17273 gives that is well-defined and continuous). (Contributed by Mario Carneiro, 14-Feb-2015.)
t t                      CovMap                                                                       t        t

Theoremcvmliftlem11 24754* Lemma for cvmlift 24758. (Contributed by Mario Carneiro, 14-Feb-2015.)
t t                      CovMap

Theoremcvmliftlem13 24755* Lemma for cvmlift 24758. The initial value of is because is a subset of which takes value at . (Contributed by Mario Carneiro, 16-Feb-2015.)
t t                      CovMap

Theoremcvmliftlem14 24756* Lemma for cvmlift 24758. Putting the results of cvmliftlem11 24754, cvmliftlem13 24755 and cvmliftmo 24743 together, we have that is a continuous function, satisfies and , and is equal to any other function which also has these properties, so it follows that is the unique lift of . (Contributed by Mario Carneiro, 16-Feb-2015.)
t t                      CovMap

Theoremcvmliftlem15 24757* Lemma for cvmlift 24758. Discharge the assumptions of cvmliftlem14 24756. The set of all open subsets of the unit interval such that is contained in an even covering of some open set in is a cover of by the definition of a covering map, so by the Lebesgue number lemma lebnumii 18855, there is a subdivision of the unit interval into equal parts such that each part is entirely contained within one such open set of . Then using finite choice ac6sfi 7280 to uniformly select one such subset and one even covering of each subset, we are ready to finish the proof with cvmliftlem14 24756. (Contributed by Mario Carneiro, 14-Feb-2015.)
t t                      CovMap

Theoremcvmlift 24758* One of the important properties of covering maps is that any path in the base space "lifts" to a path in the covering space such that , and given a starting point in the covering space this lift is unique. The proof is contained in cvmliftlem1 24744 thru cvmliftlem15 24757. (Contributed by Mario Carneiro, 16-Feb-2015.)
CovMap

Theoremcvmfo 24759 A covering map is an onto function. (Contributed by Mario Carneiro, 13-Feb-2015.)
CovMap

Theoremcvmliftiota 24760* Write out a function that is the unique lift of . (Contributed by Mario Carneiro, 16-Feb-2015.)
CovMap

Theoremcvmlift2lem1 24761* Lemma for cvmlift2 24775. (Contributed by Mario Carneiro, 1-Jun-2015.)

Theoremcvmlift2lem9a 24762* Lemma for cvmlift2 24775 and cvmlift3 24787. (Contributed by Mario Carneiro, 9-Jul-2015.)
t t        CovMap                                                                t

Theoremcvmlift2lem2 24763* Lemma for cvmlift2 24775. (Contributed by Mario Carneiro, 7-May-2015.)
CovMap

Theoremcvmlift2lem3 24764* Lemma for cvmlift2 24775. (Contributed by Mario Carneiro, 7-May-2015.)
CovMap

Theoremcvmlift2lem4 24765* Lemma for cvmlift2 24775. (Contributed by Mario Carneiro, 1-Jun-2015.)
CovMap

Theoremcvmlift2lem5 24766* Lemma for cvmlift2 24775. (Contributed by Mario Carneiro, 7-May-2015.)
CovMap

Theoremcvmlift2lem6 24767* Lemma for cvmlift2 24775. (Contributed by Mario Carneiro, 7-May-2015.)
CovMap                                           t

Theoremcvmlift2lem7 24768* Lemma for cvmlift2 24775. (Contributed by Mario Carneiro, 7-May-2015.)
CovMap

Theoremcvmlift2lem8 24769* Lemma for cvmlift2 24775. (Contributed by Mario Carneiro, 9-Mar-2015.)
CovMap

Theoremcvmlift2lem9 24770* Lemma for cvmlift2 24775. (Contributed by Mario Carneiro, 1-Jun-2015.)
CovMap                                           t t                                    t        t                                    t               t

Theoremcvmlift2lem10 24771* Lemma for cvmlift2 24775. (Contributed by Mario Carneiro, 1-Jun-2015.)
CovMap                                           t t                      t t

Theoremcvmlift2lem11 24772* Lemma for cvmlift2 24775. (Contributed by Mario Carneiro, 1-Jun-2015.)
CovMap                                                                              t t

Theoremcvmlift2lem12 24773* Lemma for cvmlift2 24775. (Contributed by Mario Carneiro, 1-Jun-2015.)
CovMap

Theoremcvmlift2lem13 24774* Lemma for cvmlift2 24775. (Contributed by Mario Carneiro, 7-May-2015.)
CovMap

Theoremcvmlift2 24775* A two-dimensional version of cvmlift 24758. There is a unique lift of functions on the unit square which commutes with the covering map. (Contributed by Mario Carneiro, 1-Jun-2015.)
CovMap

Theoremcvmliftphtlem 24776* Lemma for cvmliftpht 24777. (Contributed by Mario Carneiro, 6-Jul-2015.)
CovMap

Theoremcvmliftpht 24777* If and are path-homotopic, then their lifts and are also path-homotopic. (Contributed by Mario Carneiro, 6-Jul-2015.)
CovMap

Theoremcvmlift3lem1 24778* Lemma for cvmlift3 24787. (Contributed by Mario Carneiro, 6-Jul-2015.)
CovMap        SCon       𝑛Locally PCon

Theoremcvmlift3lem2 24779* Lemma for cvmlift2 24775. (Contributed by Mario Carneiro, 6-Jul-2015.)
CovMap        SCon       𝑛Locally PCon

Theoremcvmlift3lem3 24780* Lemma for cvmlift2 24775. (Contributed by Mario Carneiro, 6-Jul-2015.)
CovMap        SCon       𝑛Locally PCon

Theoremcvmlift3lem4 24781* Lemma for cvmlift2 24775. (Contributed by Mario Carneiro, 6-Jul-2015.)
CovMap        SCon       𝑛Locally PCon

Theoremcvmlift3lem5 24782* Lemma for cvmlift2 24775. (Contributed by Mario Carneiro, 6-Jul-2015.)
CovMap        SCon       𝑛Locally PCon

Theoremcvmlift3lem6 24783* Lemma for cvmlift3 24787. (Contributed by Mario Carneiro, 9-Jul-2015.)
CovMap        SCon       𝑛Locally PCon                                          t t                                                                       t

Theoremcvmlift3lem7 24784* Lemma for cvmlift3 24787. (Contributed by Mario Carneiro, 9-Jul-2015.)
CovMap        SCon       𝑛Locally PCon                                          t t                                    t PCon

Theoremcvmlift3lem8 24785* Lemma for cvmlift2 24775. (Contributed by Mario Carneiro, 6-Jul-2015.)
CovMap        SCon       𝑛Locally PCon                                          t t

Theoremcvmlift3lem9 24786* Lemma for cvmlift2 24775. (Contributed by Mario Carneiro, 7-May-2015.)
CovMap        SCon       𝑛Locally PCon                                          t t

Theoremcvmlift3 24787* A general version of cvmlift 24758. If is simply connected and weakly locally path-connected, then there is a unique lift of functions on which commutes with the covering map. (Contributed by Mario Carneiro, 9-Jul-2015.)
CovMap        SCon       𝑛Locally PCon

19.4.10  Normal numbers

Theoremsnmlff 24788* The function from snmlval 24790 is a mapping from positive integers to real numbers in the range . (Contributed by Mario Carneiro, 6-Apr-2015.)

Theoremsnmlfval 24789* The function from snmlval 24790 maps to the relative density of in the first digits of the digit string of in base . (Contributed by Mario Carneiro, 6-Apr-2015.)

Theoremsnmlval 24790* The property " is simply normal in base ". A number is simply normal if each digit occurs in the base- digit string of with frequency (which is consistent with the expectation in an infinite random string of numbers selected from ). (Contributed by Mario Carneiro, 6-Apr-2015.)

Theoremsnmlflim 24791* If is simply normal, then the function of relative density of in the digit string converges to , i.e. the set of occurences of in the digit string has natural density . (Contributed by Mario Carneiro, 6-Apr-2015.)

19.4.11  Godel-sets of formulas

Syntaxcgoe 24792 The Godel-set of membership.

Syntaxcgna 24793 The Godel-set for the Sheffer stroke.

Syntaxcgol 24794 The Godel-set of universal quantification. (Note that this is not a wff.)

Syntaxcsat 24795 The satisfaction function.

Syntaxcfmla 24796 The formula set predicate.

Syntaxcsate 24797 The -satisfaction function.

Syntaxcprv 24798 The "proves" relation.

Definitiondf-goel 24799 Define the Godel-set of membership. Here the arguments correspond to vN and vP , so actually means v0 v1 , not . (Contributed by Mario Carneiro, 14-Jul-2013.)

Definitiondf-gona 24800 Define the Godel-set for the Sheffer stroke NAND. Here the arguments are also Godel-sets corresponding to smaller formulae. (Contributed by Mario Carneiro, 14-Jul-2013.)

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87