Home Intuitionistic Logic ExplorerTheorem List (p. 129 of 137) < Previous  Next > Browser slow? Try the Unicode version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 12801-12900   *Has distinct variable group(s)
TypeLabelDescription
Statement

7.2.4  Open sets of a metric space

Theoremmopnrel 12801 The class of open sets of a metric space is a relation. (Contributed by Jim Kingdon, 5-May-2023.)

Theoremmopnval 12802 An open set is a subset of a metric space which includes a ball around each of its points. Definition 1.3-2 of [Kreyszig] p. 18. The object is the family of all open sets in the metric space determined by the metric . By mopntop 12804, the open sets of a metric space form a topology , whose base set is by mopnuni 12805. (Contributed by NM, 1-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)

Theoremmopntopon 12803 The set of open sets of a metric space is a topology on . Remark in [Kreyszig] p. 19. This theorem connects the two concepts and makes available the theorems for topologies for use with metric spaces. (Contributed by Mario Carneiro, 24-Aug-2015.)
TopOn

Theoremmopntop 12804 The set of open sets of a metric space is a topology. (Contributed by NM, 28-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)

Theoremmopnuni 12805 The union of all open sets in a metric space is its underlying set. (Contributed by NM, 4-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)

Theoremelmopn 12806* The defining property of an open set of a metric space. (Contributed by NM, 1-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)

Theoremmopnfss 12807 The family of open sets of a metric space is a collection of subsets of the base set. (Contributed by NM, 3-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)

Theoremmopnm 12808 The base set of a metric space is open. Part of Theorem T1 of [Kreyszig] p. 19. (Contributed by NM, 4-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)

Theoremelmopn2 12809* A defining property of an open set of a metric space. (Contributed by NM, 5-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)

Theoremmopnss 12810 An open set of a metric space is a subspace of its base set. (Contributed by NM, 3-Sep-2006.)

Theoremisxms 12811 Express the predicate " is an extended metric space" with underlying set and distance function . (Contributed by Mario Carneiro, 2-Sep-2015.)

Theoremisxms2 12812 Express the predicate " is an extended metric space" with underlying set and distance function . (Contributed by Mario Carneiro, 2-Sep-2015.)

Theoremisms 12813 Express the predicate " is a metric space" with underlying set and distance function . (Contributed by NM, 27-Aug-2006.) (Revised by Mario Carneiro, 24-Aug-2015.)

Theoremisms2 12814 Express the predicate " is a metric space" with underlying set and distance function . (Contributed by NM, 27-Aug-2006.) (Revised by Mario Carneiro, 24-Aug-2015.)

Theoremxmstopn 12815 The topology component of an extended metric space coincides with the topology generated by the metric component. (Contributed by Mario Carneiro, 26-Aug-2015.)

Theoremmstopn 12816 The topology component of a metric space coincides with the topology generated by the metric component. (Contributed by Mario Carneiro, 26-Aug-2015.)

Theoremxmstps 12817 An extended metric space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.)

Theoremmsxms 12818 A metric space is an extended metric space. (Contributed by Mario Carneiro, 26-Aug-2015.)

Theoremmstps 12819 A metric space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.)

Theoremxmsxmet 12820 The distance function, suitably truncated, is an extended metric on . (Contributed by Mario Carneiro, 2-Sep-2015.)

Theoremmsmet 12821 The distance function, suitably truncated, is a metric on . (Contributed by Mario Carneiro, 12-Nov-2013.)

Theoremmsf 12822 The distance function of a metric space is a function into the real numbers. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)

Theoremxmsxmet2 12823 The distance function, suitably truncated, is an extended metric on . (Contributed by Mario Carneiro, 2-Oct-2015.)

Theoremmsmet2 12824 The distance function, suitably truncated, is a metric on . (Contributed by Mario Carneiro, 2-Oct-2015.)

Theoremmscl 12825 Closure of the distance function of a metric space. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 2-Oct-2015.)

Theoremxmscl 12826 Closure of the distance function of an extended metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)

Theoremxmsge0 12827 The distance function in an extended metric space is nonnegative. (Contributed by Mario Carneiro, 4-Oct-2015.)

Theoremxmseq0 12828 The distance between two points in an extended metric space is zero iff the two points are identical. (Contributed by Mario Carneiro, 2-Oct-2015.)

Theoremxmssym 12829 The distance function in an extended metric space is symmetric. (Contributed by Mario Carneiro, 2-Oct-2015.)

Theoremxmstri2 12830 Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 2-Oct-2015.)

Theoremmstri2 12831 Triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)

Theoremxmstri 12832 Triangle inequality for the distance function of a metric space. Definition 14-1.1(d) of [Gleason] p. 223. (Contributed by Mario Carneiro, 2-Oct-2015.)

Theoremmstri 12833 Triangle inequality for the distance function of a metric space. Definition 14-1.1(d) of [Gleason] p. 223. (Contributed by Mario Carneiro, 2-Oct-2015.)

Theoremxmstri3 12834 Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 2-Oct-2015.)

Theoremmstri3 12835 Triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.)

Theoremmsrtri 12836 Reverse triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.)

Theoremxmspropd 12837 Property deduction for an extended metric space. (Contributed by Mario Carneiro, 4-Oct-2015.)

Theoremmspropd 12838 Property deduction for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.)

Theoremsetsmsbasg 12839 The base set of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
sSet TopSet

Theoremsetsmsdsg 12840 The distance function of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.)
sSet TopSet

Theoremsetsmstsetg 12841 The topology of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) (Revised by Jim Kingdon, 7-May-2023.)
sSet TopSet                      TopSet

Theoremmopni 12842* An open set of a metric space includes a ball around each of its points. (Contributed by NM, 3-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.)

Theoremmopni2 12843* An open set of a metric space includes a ball around each of its points. (Contributed by NM, 2-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)

Theoremmopni3 12844* An open set of a metric space includes an arbitrarily small ball around each of its points. (Contributed by NM, 20-Sep-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)

Theoremblssopn 12845 The balls of a metric space are open sets. (Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)

Theoremunimopn 12846 The union of a collection of open sets of a metric space is open. Theorem T2 of [Kreyszig] p. 19. (Contributed by NM, 4-Sep-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)

Theoremmopnin 12847 The intersection of two open sets of a metric space is open. (Contributed by NM, 4-Sep-2006.) (Revised by Mario Carneiro, 23-Dec-2013.)

Theoremmopn0 12848 The empty set is an open set of a metric space. Part of Theorem T1 of [Kreyszig] p. 19. (Contributed by NM, 4-Sep-2006.)

Theoremrnblopn 12849 A ball of a metric space is an open set. (Contributed by NM, 12-Sep-2006.)

Theoremblopn 12850 A ball of a metric space is an open set. (Contributed by NM, 9-Mar-2007.) (Revised by Mario Carneiro, 12-Nov-2013.)

Theoremneibl 12851* The neighborhoods around a point of a metric space are those subsets containing a ball around . Definition of neighborhood in [Kreyszig] p. 19. (Contributed by NM, 8-Nov-2007.) (Revised by Mario Carneiro, 23-Dec-2013.)

Theoremblnei 12852 A ball around a point is a neighborhood of the point. (Contributed by NM, 8-Nov-2007.) (Revised by Mario Carneiro, 24-Aug-2015.)

Theoremblsscls2 12853* A smaller closed ball is contained in a larger open ball. (Contributed by Mario Carneiro, 10-Jan-2014.)

Theoremmetss 12854* Two ways of saying that metric generates a finer topology than metric . (Contributed by Mario Carneiro, 12-Nov-2013.) (Revised by Mario Carneiro, 24-Aug-2015.)

Theoremmetequiv 12855* Two ways of saying that two metrics generate the same topology. Two metrics satisfying the right-hand side are said to be (topologically) equivalent. (Contributed by Jeff Hankins, 21-Jun-2009.) (Revised by Mario Carneiro, 12-Nov-2013.)

Theoremmetequiv2 12856* If there is a sequence of radii approaching zero for which the balls of both metrics coincide, then the generated topologies are equivalent. (Contributed by Mario Carneiro, 26-Aug-2015.)

Theoremmetss2lem 12857* Lemma for metss2 12858. (Contributed by Mario Carneiro, 14-Sep-2015.)

Theoremmetss2 12858* If the metric is "strongly finer" than (meaning that there is a positive real constant such that ), then generates a finer topology. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then they generate the same topology.) (Contributed by Mario Carneiro, 14-Sep-2015.)

Theoremcomet 12859* The composition of an extended metric with a monotonic subadditive function is an extended metric. (Contributed by Mario Carneiro, 21-Mar-2015.)

Theorembdmetval 12860* Value of the standard bounded metric. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 9-May-2023.)
inf        inf

Theorembdxmet 12861* The standard bounded metric is an extended metric given an extended metric and a positive extended real cutoff. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 9-May-2023.)
inf

Theorembdmet 12862* The standard bounded metric is a proper metric given an extended metric and a positive real cutoff. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 19-May-2023.)
inf

Theorembdbl 12863* The standard bounded metric corresponding to generates the same balls as for radii less than . (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 19-May-2023.)
inf

Theorembdmopn 12864* The standard bounded metric corresponding to generates the same topology as . (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 19-May-2023.)
inf

Theoremmopnex 12865* The topology generated by an extended metric can also be generated by a true metric. Thus, "metrizable topologies" can equivalently be defined in terms of metrics or extended metrics. (Contributed by Mario Carneiro, 26-Aug-2015.)

Theoremmetrest 12866 Two alternate formulations of a subspace topology of a metric space topology. (Contributed by Jeff Hankins, 19-Aug-2009.) (Proof shortened by Mario Carneiro, 5-Jan-2014.)
t

Theoremxmetxp 12867* The maximum metric (Chebyshev distance) on the product of two sets. (Contributed by Jim Kingdon, 11-Oct-2023.)

Theoremxmetxpbl 12868* The maximum metric (Chebyshev distance) on the product of two sets, expressed in terms of balls centered on a point with radius . (Contributed by Jim Kingdon, 22-Oct-2023.)

Theoremxmettxlem 12869* Lemma for xmettx 12870. (Contributed by Jim Kingdon, 15-Oct-2023.)

Theoremxmettx 12870* The maximum metric (Chebyshev distance) on the product of two sets, expressed as a binary topological product. (Contributed by Jim Kingdon, 11-Oct-2023.)

7.2.5  Continuity in metric spaces

Theoremmetcnp3 12871* Two ways to express that is continuous at for metric spaces. Proposition 14-4.2 of [Gleason] p. 240. (Contributed by NM, 17-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)

Theoremmetcnp 12872* Two ways to say a mapping from metric to metric is continuous at point . (Contributed by NM, 11-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)

Theoremmetcnp2 12873* Two ways to say a mapping from metric to metric is continuous at point . The distance arguments are swapped compared to metcnp 12872 (and Munkres' metcn 12874) for compatibility with df-lm 12550. Definition 1.3-3 of [Kreyszig] p. 20. (Contributed by NM, 4-Jun-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)

Theoremmetcn 12874* Two ways to say a mapping from metric to metric is continuous. Theorem 10.1 of [Munkres] p. 127. The second biconditional argument says that for every positive "epsilon" there is a positive "delta" such that a distance less than delta in maps to a distance less than epsilon in . (Contributed by NM, 15-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.)

Theoremmetcnpi 12875* Epsilon-delta property of a continuous metric space function, with function arguments as in metcnp 12872. (Contributed by NM, 17-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)

Theoremmetcnpi2 12876* Epsilon-delta property of a continuous metric space function, with swapped distance function arguments as in metcnp2 12873. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)

Theoremmetcnpi3 12877* Epsilon-delta property of a metric space function continuous at . A variation of metcnpi2 12876 with non-strict ordering. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)

Theoremtxmetcnp 12878* Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.) (Revised by Jim Kingdon, 22-Oct-2023.)

Theoremtxmetcn 12879* Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.)

Theoremmetcnpd 12880* Two ways to say a mapping from metric to metric is continuous at point . (Contributed by Jim Kingdon, 14-Jun-2023.)

7.2.6  Topology on the reals

Theoremqtopbasss 12881* The set of open intervals with endpoints in a subset forms a basis for a topology. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by Jim Kingdon, 22-May-2023.)
inf

Theoremqtopbas 12882 The set of open intervals with rational endpoints forms a basis for a topology. (Contributed by NM, 8-Mar-2007.)

Theoremretopbas 12883 A basis for the standard topology on the reals. (Contributed by NM, 6-Feb-2007.) (Proof shortened by Mario Carneiro, 17-Jun-2014.)

Theoremretop 12884 The standard topology on the reals. (Contributed by FL, 4-Jun-2007.)

Theoremuniretop 12885 The underlying set of the standard topology on the reals is the reals. (Contributed by FL, 4-Jun-2007.)

Theoremretopon 12886 The standard topology on the reals is a topology on the reals. (Contributed by Mario Carneiro, 28-Aug-2015.)
TopOn

Theoremretps 12887 The standard topological space on the reals. (Contributed by NM, 19-Oct-2012.)
TopSet

Theoremiooretopg 12888 Open intervals are open sets of the standard topology on the reals . (Contributed by FL, 18-Jun-2007.) (Revised by Jim Kingdon, 23-May-2023.)

Theoremcnmetdval 12889 Value of the distance function of the metric space of complex numbers. (Contributed by NM, 9-Dec-2006.) (Revised by Mario Carneiro, 27-Dec-2014.)

Theoremcnmet 12890 The absolute value metric determines a metric space on the complex numbers. This theorem provides a link between complex numbers and metrics spaces, making metric space theorems available for use with complex numbers. (Contributed by FL, 9-Oct-2006.)

Theoremcnxmet 12891 The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.)

Theoremcntoptopon 12892 The topology of the complex numbers is a topology. (Contributed by Jim Kingdon, 6-Jun-2023.)
TopOn

Theoremcntoptop 12893 The topology of the complex numbers is a topology. (Contributed by Jim Kingdon, 6-Jun-2023.)

Theoremcnbl0 12894 Two ways to write the open ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.)

Theoremcnblcld 12895* Two ways to write the closed ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.)

Theoremunicntopcntop 12896 The underlying set of the standard topology on the complex numbers is the set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by Jim Kingdon, 12-Dec-2023.)

Theoremcnopncntop 12897 The set of complex numbers is open with respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by Jim Kingdon, 12-Dec-2023.)

Theoremreopnap 12898* The real numbers apart from a given real number form an open set. (Contributed by Jim Kingdon, 13-Dec-2023.)
#

Theoremremetdval 12899 Value of the distance function of the metric space of real numbers. (Contributed by NM, 16-May-2007.)

Theoremremet 12900 The absolute value metric determines a metric space on the reals. (Contributed by NM, 10-Feb-2007.)

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 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13614
 Copyright terms: Public domain < Previous  Next >