Home | Metamath
Proof Explorer Theorem List (p. 239 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | met2ndc 23801* | A metric space is second-countable iff it is separable (has a countable dense subset). (Contributed by Mario Carneiro, 13-Apr-2015.) |
β’ π½ = (MetOpenβπ·) β β’ (π· β (βMetβπ) β (π½ β 2ndΟ β βπ₯ β π« π(π₯ βΌ Ο β§ ((clsβπ½)βπ₯) = π))) | ||
Theorem | metrest 23802 | 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.) |
β’ π· = (πΆ βΎ (π Γ π)) & β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) β β’ ((πΆ β (βMetβπ) β§ π β π) β (π½ βΎt π) = πΎ) | ||
Theorem | ressxms 23803 | The restriction of a metric space is a metric space. (Contributed by Mario Carneiro, 24-Aug-2015.) |
β’ ((πΎ β βMetSp β§ π΄ β π) β (πΎ βΎs π΄) β βMetSp) | ||
Theorem | ressms 23804 | The restriction of a metric space is a metric space. (Contributed by Mario Carneiro, 24-Aug-2015.) |
β’ ((πΎ β MetSp β§ π΄ β π) β (πΎ βΎs π΄) β MetSp) | ||
Theorem | prdsmslem1 23805 | Lemma for prdsms 23809. The distance function of a product structure is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ π = (πXsπ ) & β’ (π β π β π) & β’ (π β πΌ β Fin) & β’ π· = (distβπ) & β’ π΅ = (Baseβπ) & β’ (π β π :πΌβΆMetSp) β β’ (π β π· β (Metβπ΅)) | ||
Theorem | prdsxmslem1 23806 | Lemma for prdsms 23809. The distance function of a product structure is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ π = (πXsπ ) & β’ (π β π β π) & β’ (π β πΌ β Fin) & β’ π· = (distβπ) & β’ π΅ = (Baseβπ) & β’ (π β π :πΌβΆβMetSp) β β’ (π β π· β (βMetβπ΅)) | ||
Theorem | prdsxmslem2 23807* | Lemma for prdsxms 23808. The topology generated by the supremum metric is the same as the product topology, when the index set is finite. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ π = (πXsπ ) & β’ (π β π β π) & β’ (π β πΌ β Fin) & β’ π· = (distβπ) & β’ π΅ = (Baseβπ) & β’ (π β π :πΌβΆβMetSp) & β’ π½ = (TopOpenβπ) & β’ π = (Baseβ(π βπ)) & β’ πΈ = ((distβ(π βπ)) βΎ (π Γ π)) & β’ πΎ = (TopOpenβ(π βπ)) & β’ πΆ = {π₯ β£ βπ((π Fn πΌ β§ βπ β πΌ (πβπ) β ((TopOpen β π )βπ) β§ βπ§ β Fin βπ β (πΌ β π§)(πβπ) = βͺ ((TopOpen β π )βπ)) β§ π₯ = Xπ β πΌ (πβπ))} β β’ (π β π½ = (MetOpenβπ·)) | ||
Theorem | prdsxms 23808 | The indexed product structure is an extended metric space when the index set is finite. (Although the extended metric is still valid when the index set is infinite, it no longer agrees with the product topology, which is not metrizable in any case.) (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ π = (πXsπ ) β β’ ((π β π β§ πΌ β Fin β§ π :πΌβΆβMetSp) β π β βMetSp) | ||
Theorem | prdsms 23809 | The indexed product structure is a metric space when the index set is finite. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ π = (πXsπ ) β β’ ((π β π β§ πΌ β Fin β§ π :πΌβΆMetSp) β π β MetSp) | ||
Theorem | pwsxms 23810 | A power of an extended metric space is an extended metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ π = (π βs πΌ) β β’ ((π β βMetSp β§ πΌ β Fin) β π β βMetSp) | ||
Theorem | pwsms 23811 | A power of a metric space is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ π = (π βs πΌ) β β’ ((π β MetSp β§ πΌ β Fin) β π β MetSp) | ||
Theorem | xpsxms 23812 | A binary product of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ π = (π Γs π) β β’ ((π β βMetSp β§ π β βMetSp) β π β βMetSp) | ||
Theorem | xpsms 23813 | A binary product of metric spaces is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
β’ π = (π Γs π) β β’ ((π β MetSp β§ π β MetSp) β π β MetSp) | ||
Theorem | tmsxps 23814 | Express the product of two metrics as another metric. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π = (distβ((toMetSpβπ) Γs (toMetSpβπ))) & β’ (π β π β (βMetβπ)) & β’ (π β π β (βMetβπ)) β β’ (π β π β (βMetβ(π Γ π))) | ||
Theorem | tmsxpsmopn 23815 | Express the product of two metrics as another metric. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π = (distβ((toMetSpβπ) Γs (toMetSpβπ))) & β’ (π β π β (βMetβπ)) & β’ (π β π β (βMetβπ)) & β’ π½ = (MetOpenβπ) & β’ πΎ = (MetOpenβπ) & β’ πΏ = (MetOpenβπ) β β’ (π β πΏ = (π½ Γt πΎ)) | ||
Theorem | tmsxpsval 23816 | Value of the product of two metrics. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π = (distβ((toMetSpβπ) Γs (toMetSpβπ))) & β’ (π β π β (βMetβπ)) & β’ (π β π β (βMetβπ)) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (β¨π΄, π΅β©πβ¨πΆ, π·β©) = sup({(π΄ππΆ), (π΅ππ·)}, β*, < )) | ||
Theorem | tmsxpsval2 23817 | Value of the product of two metrics. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π = (distβ((toMetSpβπ) Γs (toMetSpβπ))) & β’ (π β π β (βMetβπ)) & β’ (π β π β (βMetβπ)) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) & β’ (π β π· β π) β β’ (π β (β¨π΄, π΅β©πβ¨πΆ, π·β©) = if((π΄ππΆ) β€ (π΅ππ·), (π΅ππ·), (π΄ππΆ))) | ||
Theorem | metcnp3 23818* | 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.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) β β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β β+ βπ§ β β+ (πΉ β (π(ballβπΆ)π§)) β ((πΉβπ)(ballβπ·)π¦)))) | ||
Theorem | metcnp 23819* | 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.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) β β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β β+ βπ§ β β+ βπ€ β π ((ππΆπ€) < π§ β ((πΉβπ)π·(πΉβπ€)) < π¦)))) | ||
Theorem | metcnp2 23820* | Two ways to say a mapping from metric πΆ to metric π· is continuous at point π. The distance arguments are swapped compared to metcnp 23819 (and Munkres' metcn 23821) for compatibility with df-lm 22502. Definition 1.3-3 of [Kreyszig] p. 20. (Contributed by NM, 4-Jun-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) β β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β β+ βπ§ β β+ βπ€ β π ((π€πΆπ) < π§ β ((πΉβπ€)π·(πΉβπ)) < π¦)))) | ||
Theorem | metcn 23821* | 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.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) β β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ₯ β π βπ¦ β β+ βπ§ β β+ βπ€ β π ((π₯πΆπ€) < π§ β ((πΉβπ₯)π·(πΉβπ€)) < π¦)))) | ||
Theorem | metcnpi 23822* | Epsilon-delta property of a continuous metric space function, with function arguments as in metcnp 23819. (Contributed by NM, 17-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) β β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β βπ₯ β β+ βπ¦ β π ((ππΆπ¦) < π₯ β ((πΉβπ)π·(πΉβπ¦)) < π΄)) | ||
Theorem | metcnpi2 23823* | Epsilon-delta property of a continuous metric space function, with swapped distance function arguments as in metcnp2 23820. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) β β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β βπ₯ β β+ βπ¦ β π ((π¦πΆπ) < π₯ β ((πΉβπ¦)π·(πΉβπ)) < π΄)) | ||
Theorem | metcnpi3 23824* | Epsilon-delta property of a metric space function continuous at π. A variation of metcnpi2 23823 with non-strict ordering. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) β β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ)) β§ (πΉ β ((π½ CnP πΎ)βπ) β§ π΄ β β+)) β βπ₯ β β+ βπ¦ β π ((π¦πΆπ) β€ π₯ β ((πΉβπ¦)π·(πΉβπ)) β€ π΄)) | ||
Theorem | txmetcnp 23825* | Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) & β’ πΏ = (MetOpenβπΈ) β β’ (((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β§ (π΄ β π β§ π΅ β π)) β (πΉ β (((π½ Γt πΎ) CnP πΏ)ββ¨π΄, π΅β©) β (πΉ:(π Γ π)βΆπ β§ βπ§ β β+ βπ€ β β+ βπ’ β π βπ£ β π (((π΄πΆπ’) < π€ β§ (π΅π·π£) < π€) β ((π΄πΉπ΅)πΈ(π’πΉπ£)) < π§)))) | ||
Theorem | txmetcn 23826* | Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) & β’ πΏ = (MetOpenβπΈ) β β’ ((πΆ β (βMetβπ) β§ π· β (βMetβπ) β§ πΈ β (βMetβπ)) β (πΉ β ((π½ Γt πΎ) Cn πΏ) β (πΉ:(π Γ π)βΆπ β§ βπ₯ β π βπ¦ β π βπ§ β β+ βπ€ β β+ βπ’ β π βπ£ β π (((π₯πΆπ’) < π€ β§ (π¦π·π£) < π€) β ((π₯πΉπ¦)πΈ(π’πΉπ£)) < π§)))) | ||
Theorem | metuval 23827* | Value of the uniform structure generated by metric π·. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ (π· β (PsMetβπ) β (metUnifβπ·) = ((π Γ π)filGenran (π β β+ β¦ (β‘π· β (0[,)π))))) | ||
Theorem | metustel 23828* | Define a filter base πΉ generated by a metric π·. (Contributed by Thierry Arnoux, 22-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) β β’ (π· β (PsMetβπ) β (π΅ β πΉ β βπ β β+ π΅ = (β‘π· β (0[,)π)))) | ||
Theorem | metustss 23829* | Range of the elements of the filter base generated by the metric π·. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) β β’ ((π· β (PsMetβπ) β§ π΄ β πΉ) β π΄ β (π Γ π)) | ||
Theorem | metustrel 23830* | Elements of the filter base generated by the metric π· are relations. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) β β’ ((π· β (PsMetβπ) β§ π΄ β πΉ) β Rel π΄) | ||
Theorem | metustto 23831* | Any two elements of the filter base generated by the metric π· can be compared, like for RR+ (i.e. it's totally ordered). (Contributed by Thierry Arnoux, 22-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) β β’ ((π· β (PsMetβπ) β§ π΄ β πΉ β§ π΅ β πΉ) β (π΄ β π΅ β¨ π΅ β π΄)) | ||
Theorem | metustid 23832* | The identity diagonal is included in all elements of the filter base generated by the metric π·. (Contributed by Thierry Arnoux, 22-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) β β’ ((π· β (PsMetβπ) β§ π΄ β πΉ) β ( I βΎ π) β π΄) | ||
Theorem | metustsym 23833* | Elements of the filter base generated by the metric π· are symmetric. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) β β’ ((π· β (PsMetβπ) β§ π΄ β πΉ) β β‘π΄ = π΄) | ||
Theorem | metustexhalf 23834* | For any element π΄ of the filter base generated by the metric π·, the half element (corresponding to half the distance) is also in this base. (Contributed by Thierry Arnoux, 28-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) β β’ (((π β β β§ π· β (PsMetβπ)) β§ π΄ β πΉ) β βπ£ β πΉ (π£ β π£) β π΄) | ||
Theorem | metustfbas 23835* | The filter base generated by a metric π·. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) β β’ ((π β β β§ π· β (PsMetβπ)) β πΉ β (fBasβ(π Γ π))) | ||
Theorem | metust 23836* | The uniform structure generated by a metric π·. (Contributed by Thierry Arnoux, 26-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) β β’ ((π β β β§ π· β (PsMetβπ)) β ((π Γ π)filGenπΉ) β (UnifOnβπ)) | ||
Theorem | cfilucfil 23837* | Given a metric π· and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the filter bases which contain balls of any pre-chosen size. See iscfil 24551. (Contributed by Thierry Arnoux, 29-Nov-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ πΉ = ran (π β β+ β¦ (β‘π· β (0[,)π))) β β’ ((π β β β§ π· β (PsMetβπ)) β (πΆ β (CauFiluβ((π Γ π)filGenπΉ)) β (πΆ β (fBasβπ) β§ βπ₯ β β+ βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯)))) | ||
Theorem | metuust 23838 | The uniform structure generated by metric π· is a uniform structure. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ ((π β β β§ π· β (PsMetβπ)) β (metUnifβπ·) β (UnifOnβπ)) | ||
Theorem | cfilucfil2 23839* | Given a metric π· and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the filter bases which contain balls of any pre-chosen size. See iscfil 24551. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ ((π β β β§ π· β (PsMetβπ)) β (πΆ β (CauFiluβ(metUnifβπ·)) β (πΆ β (fBasβπ) β§ βπ₯ β β+ βπ¦ β πΆ (π· β (π¦ Γ π¦)) β (0[,)π₯)))) | ||
Theorem | blval2 23840 | The ball around a point π, alternative definition. (Contributed by Thierry Arnoux, 7-Dec-2017.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
β’ ((π· β (PsMetβπ) β§ π β π β§ π β β+) β (π(ballβπ·)π ) = ((β‘π· β (0[,)π )) β {π})) | ||
Theorem | elbl4 23841 | Membership in a ball, alternative definition. (Contributed by Thierry Arnoux, 26-Jan-2018.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
β’ (((π· β (PsMetβπ) β§ π β β+) β§ (π΄ β π β§ π΅ β π)) β (π΅ β (π΄(ballβπ·)π ) β π΅(β‘π· β (0[,)π ))π΄)) | ||
Theorem | metuel 23842* | Elementhood in the uniform structure generated by a metric π· (Contributed by Thierry Arnoux, 8-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ ((π β β β§ π· β (PsMetβπ)) β (π β (metUnifβπ·) β (π β (π Γ π) β§ βπ€ β ran (π β β+ β¦ (β‘π· β (0[,)π)))π€ β π))) | ||
Theorem | metuel2 23843* | Elementhood in the uniform structure generated by a metric π· (Contributed by Thierry Arnoux, 24-Jan-2018.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ π = (metUnifβπ·) β β’ ((π β β β§ π· β (PsMetβπ)) β (π β π β (π β (π Γ π) β§ βπ β β+ βπ₯ β π βπ¦ β π ((π₯π·π¦) < π β π₯ππ¦)))) | ||
Theorem | metustbl 23844* | The "section" image of an entourage at a point π always contains a ball (centered on this point). (Contributed by Thierry Arnoux, 8-Dec-2017.) |
β’ ((π· β (PsMetβπ) β§ π β (metUnifβπ·) β§ π β π) β βπ β ran (ballβπ·)(π β π β§ π β (π β {π}))) | ||
Theorem | psmetutop 23845 | The topology induced by a uniform structure generated by a metric π· is generated by that metric's open balls. (Contributed by Thierry Arnoux, 6-Dec-2017.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
β’ ((π β β β§ π· β (PsMetβπ)) β (unifTopβ(metUnifβπ·)) = (topGenβran (ballβπ·))) | ||
Theorem | xmetutop 23846 | The topology induced by a uniform structure generated by an extended metric π· is that metric's open sets. (Contributed by Thierry Arnoux, 11-Mar-2018.) |
β’ ((π β β β§ π· β (βMetβπ)) β (unifTopβ(metUnifβπ·)) = (MetOpenβπ·)) | ||
Theorem | xmsusp 23847 | If the uniform set of a metric space is the uniform structure generated by its metric, then it is a uniform space. (Contributed by Thierry Arnoux, 14-Dec-2017.) |
β’ π = (BaseβπΉ) & β’ π· = ((distβπΉ) βΎ (π Γ π)) & β’ π = (UnifStβπΉ) β β’ ((π β β β§ πΉ β βMetSp β§ π = (metUnifβπ·)) β πΉ β UnifSp) | ||
Theorem | restmetu 23848 | The uniform structure generated by the restriction of a metric is its trace. (Contributed by Thierry Arnoux, 18-Dec-2017.) |
β’ ((π΄ β β β§ π· β (PsMetβπ) β§ π΄ β π) β ((metUnifβπ·) βΎt (π΄ Γ π΄)) = (metUnifβ(π· βΎ (π΄ Γ π΄)))) | ||
Theorem | metucn 23849* | Uniform continuity in metric spaces. Compare the order of the quantifiers with metcn 23821. (Contributed by Thierry Arnoux, 26-Jan-2018.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ π = (metUnifβπΆ) & β’ π = (metUnifβπ·) & β’ (π β π β β ) & β’ (π β π β β ) & β’ (π β πΆ β (PsMetβπ)) & β’ (π β π· β (PsMetβπ)) β β’ (π β (πΉ β (π Cnuπ) β (πΉ:πβΆπ β§ βπ β β+ βπ β β+ βπ₯ β π βπ¦ β π ((π₯πΆπ¦) < π β ((πΉβπ₯)π·(πΉβπ¦)) < π)))) | ||
Theorem | dscmet 23850* | The discrete metric on any set π. Definition 1.1-8 of [Kreyszig] p. 8. (Contributed by FL, 12-Oct-2006.) |
β’ π· = (π₯ β π, π¦ β π β¦ if(π₯ = π¦, 0, 1)) β β’ (π β π β π· β (Metβπ)) | ||
Theorem | dscopn 23851* | The discrete metric generates the discrete topology. In particular, the discrete topology is metrizable. (Contributed by Mario Carneiro, 29-Jan-2014.) |
β’ π· = (π₯ β π, π¦ β π β¦ if(π₯ = π¦, 0, 1)) β β’ (π β π β (MetOpenβπ·) = π« π) | ||
Theorem | nrmmetd 23852* | Show that a group norm generates a metric. Part of Definition 2.2-1 of [Kreyszig] p. 58. (Contributed by NM, 4-Dec-2006.) (Revised by Mario Carneiro, 2-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ β = (-gβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β Grp) & β’ (π β πΉ:πβΆβ) & β’ ((π β§ π₯ β π) β ((πΉβπ₯) = 0 β π₯ = 0 )) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (πΉβ(π₯ β π¦)) β€ ((πΉβπ₯) + (πΉβπ¦))) β β’ (π β (πΉ β β ) β (Metβπ)) | ||
Theorem | abvmet 23853 | An absolute value πΉ generates a metric defined by π(π₯, π¦) = πΉ(π₯ β π¦), analogously to cnmet 24057. (In fact, the ring structure is not needed at all; the group properties abveq0 20208 and abvtri 20212, abvneg 20216 are sufficient.) (Contributed by Mario Carneiro, 9-Sep-2014.) (Revised by Mario Carneiro, 2-Oct-2015.) |
β’ π = (Baseβπ ) & β’ π΄ = (AbsValβπ ) & β’ β = (-gβπ ) β β’ (πΉ β π΄ β (πΉ β β ) β (Metβπ)) | ||
In the following, the norm of a normed algebraic structure (group, left module, vector space) is defined by the (given) distance function (the norm π of an element is its distance π· from the zero element, see nmval 23867: (πβπ΄) = (π΄π· 0 )). By this definition, the norm function π is actually a norm (satisfying the properties: being a function into the reals; subadditivity/triangle inequality (πβ(π₯ + π¦)) β€ ((πβπ₯) + (πβπ¦)); absolute homogeneity ( n(sx) = |s| n(x) ) [Remark: for group norms, some authors (e.g., Juris Steprans in "A characterization of free abelian groups") demand that n(sx) = |s| n(x) for all π β β€, whereas other authors (e.g., N. H. Bingham and A. J. Ostaszewski in "Normed versus topological groups: Dichotomy and duality") only require inversion symmetry, i.e., (πβ( β π₯) = πβπ₯). The definition df-ngp 23861 of a group norm follows the second aproach, see nminv 23899.] and positive definiteness/point-separation ((πβπ₯) = 0 β π₯ = 0)) if the structure is a metric space with a right-translation-invariant metric (see nmf 23893, nmtri 23904, nmvs 23962 and nmeq0 23896). An alternate definition of a normed group (i.e., a group equipped with a norm) not using the properties of a metric space is given by Theorem tngngp3 23942. The norm can be expressed as the distance to zero (nmfval 23866), so in a structure with a zero (a "pointed set", for instance a monoid or a group), the norm can be expressed as the distance restricted to the elements of the base set to zero (nmfval0 23868). Usually, however, the norm of a normed structure is given, and the corresponding metric ("induced metric") is defined as the distance function based on the norm (the distance π· between two elements is the norm π of their difference, see ngpds 23882: (π΄π·π΅) = (πβ(π΄ β π΅))). The operation toNrmGrp does exactly this, i.e., it adds a distance function (and a topology) to a structure (which should be at least a group for the difference of two elements to make sense) corresponding to a given norm as explained above: (distβπ) = (π β β ), see also tngds 23933. By this, the enhanced structure becomes a normed structure if the induced metric is in fact a metric (see tngngp2 23938) or a norm (see tngngpd 23939). If the norm is derived from a given metric, as done with df-nm 23860, the induced metric is the original metric restricted to the base set: (distβπ) = ((distβπΊ) βΎ (π Γ π)), see nrmtngdist 23943, and the norm remains the same: (normβπ) = (normβπΊ), see nrmtngnrm 23944. | ||
Syntax | cnm 23854 | Norm of a normed ring. |
class norm | ||
Syntax | cngp 23855 | The class of all normed groups. |
class NrmGrp | ||
Syntax | ctng 23856 | Make a normed group from a norm and a group. |
class toNrmGrp | ||
Syntax | cnrg 23857 | Normed ring. |
class NrmRing | ||
Syntax | cnlm 23858 | Normed module. |
class NrmMod | ||
Syntax | cnvc 23859 | Normed vector space. |
class NrmVec | ||
Definition | df-nm 23860* | Define the norm on a group or ring (when it makes sense) in terms of the distance to zero. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ norm = (π€ β V β¦ (π₯ β (Baseβπ€) β¦ (π₯(distβπ€)(0gβπ€)))) | ||
Definition | df-ngp 23861 | Define a normed group, which is a group with a right-translation-invariant metric. This is not a standard notion, but is helpful as the most general context in which a metric-like norm makes sense. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ NrmGrp = {π β (Grp β© MetSp) β£ ((normβπ) β (-gβπ)) β (distβπ)} | ||
Definition | df-tng 23862* | Define a function that fills in the topology and metric components of a structure given a group and a norm on it. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ toNrmGrp = (π β V, π β V β¦ ((π sSet β¨(distβndx), (π β (-gβπ))β©) sSet β¨(TopSetβndx), (MetOpenβ(π β (-gβπ)))β©)) | ||
Definition | df-nrg 23863 | A normed ring is a ring with an induced topology and metric such that the metric is translation-invariant and the norm (distance from 0) is an absolute value on the ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ NrmRing = {π€ β NrmGrp β£ (normβπ€) β (AbsValβπ€)} | ||
Definition | df-nlm 23864* | A normed (left) module is a module which is also a normed group over a normed ring, such that the norm distributes over scalar multiplication. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ NrmMod = {π€ β (NrmGrp β© LMod) β£ [(Scalarβπ€) / π](π β NrmRing β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ€)((normβπ€)β(π₯( Β·π βπ€)π¦)) = (((normβπ)βπ₯) Β· ((normβπ€)βπ¦)))} | ||
Definition | df-nvc 23865 | A normed vector space is a normed module which is also a vector space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ NrmVec = (NrmMod β© LVec) | ||
Theorem | nmfval 23866* | The value of the norm function as the distance to zero. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (normβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π· = (distβπ) β β’ π = (π₯ β π β¦ (π₯π· 0 )) | ||
Theorem | nmval 23867 | The value of the norm as the distance to zero. Problem 1 of [Kreyszig] p. 63. (Contributed by NM, 4-Dec-2006.) (Revised by Mario Carneiro, 2-Oct-2015.) |
β’ π = (normβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π· = (distβπ) β β’ (π΄ β π β (πβπ΄) = (π΄π· 0 )) | ||
Theorem | nmfval0 23868* | The value of the norm function on a structure containing a zero as the distance restricted to the elements of the base set to zero. Examples of structures containing a "zero" are groups (see nmfval2 23869 proved from this theorem and grpidcl 18713) or more generally monoids (see mndidcl 18506), or pointed sets). (Contributed by Mario Carneiro, 2-Oct-2015.) Extract this result from the proof of nmfval2 23869. (Revised by BJ, 27-Aug-2024.) |
β’ π = (normβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π· = (distβπ) & β’ πΈ = (π· βΎ (π Γ π)) β β’ ( 0 β π β π = (π₯ β π β¦ (π₯πΈ 0 ))) | ||
Theorem | nmfval2 23869* | The value of the norm function on a group as the distance restricted to the elements of the base set to zero. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (normβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π· = (distβπ) & β’ πΈ = (π· βΎ (π Γ π)) β β’ (π β Grp β π = (π₯ β π β¦ (π₯πΈ 0 ))) | ||
Theorem | nmval2 23870 | The value of the norm on a group as the distance restricted to the elements of the base set to zero. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (normβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π· = (distβπ) & β’ πΈ = (π· βΎ (π Γ π)) β β’ ((π β Grp β§ π΄ β π) β (πβπ΄) = (π΄πΈ 0 )) | ||
Theorem | nmf2 23871 | The norm on a metric group is a function from the base set into the reals. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (normβπ) & β’ π = (Baseβπ) & β’ π· = (distβπ) & β’ πΈ = (π· βΎ (π Γ π)) β β’ ((π β Grp β§ πΈ β (Metβπ)) β π:πβΆβ) | ||
Theorem | nmpropd 23872 | Weak property deduction for a norm. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β (BaseβπΎ) = (BaseβπΏ)) & β’ (π β (+gβπΎ) = (+gβπΏ)) & β’ (π β (distβπΎ) = (distβπΏ)) β β’ (π β (normβπΎ) = (normβπΏ)) | ||
Theorem | nmpropd2 23873* | Strong property deduction for a norm. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ (π β πΎ β Grp) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) & β’ (π β ((distβπΎ) βΎ (π΅ Γ π΅)) = ((distβπΏ) βΎ (π΅ Γ π΅))) β β’ (π β (normβπΎ) = (normβπΏ)) | ||
Theorem | isngp 23874 | The property of being a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (normβπΊ) & β’ β = (-gβπΊ) & β’ π· = (distβπΊ) β β’ (πΊ β NrmGrp β (πΊ β Grp β§ πΊ β MetSp β§ (π β β ) β π·)) | ||
Theorem | isngp2 23875 | The property of being a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (normβπΊ) & β’ β = (-gβπΊ) & β’ π· = (distβπΊ) & β’ π = (BaseβπΊ) & β’ πΈ = (π· βΎ (π Γ π)) β β’ (πΊ β NrmGrp β (πΊ β Grp β§ πΊ β MetSp β§ (π β β ) = πΈ)) | ||
Theorem | isngp3 23876* | The property of being a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (normβπΊ) & β’ β = (-gβπΊ) & β’ π· = (distβπΊ) & β’ π = (BaseβπΊ) β β’ (πΊ β NrmGrp β (πΊ β Grp β§ πΊ β MetSp β§ βπ₯ β π βπ¦ β π (π₯π·π¦) = (πβ(π₯ β π¦)))) | ||
Theorem | ngpgrp 23877 | A normed group is a group. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ (πΊ β NrmGrp β πΊ β Grp) | ||
Theorem | ngpms 23878 | A normed group is a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ (πΊ β NrmGrp β πΊ β MetSp) | ||
Theorem | ngpxms 23879 | A normed group is an extended metric space. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ (πΊ β NrmGrp β πΊ β βMetSp) | ||
Theorem | ngptps 23880 | A normed group is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015.) |
β’ (πΊ β NrmGrp β πΊ β TopSp) | ||
Theorem | ngpmet 23881 | The (induced) metric of a normed group is a metric. Part of Definition 2.2-1 of [Kreyszig] p. 58. (Contributed by NM, 4-Dec-2006.) (Revised by AV, 14-Oct-2021.) |
β’ π = (BaseβπΊ) & β’ π· = ((distβπΊ) βΎ (π Γ π)) β β’ (πΊ β NrmGrp β π· β (Metβπ)) | ||
Theorem | ngpds 23882 | Value of the distance function in terms of the norm of a normed group. Equation 1 of [Kreyszig] p. 59. (Contributed by NM, 28-Nov-2006.) (Revised by Mario Carneiro, 2-Oct-2015.) |
β’ π = (normβπΊ) & β’ π = (BaseβπΊ) & β’ β = (-gβπΊ) & β’ π· = (distβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = (πβ(π΄ β π΅))) | ||
Theorem | ngpdsr 23883 | Value of the distance function in terms of the norm of a normed group. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (normβπΊ) & β’ π = (BaseβπΊ) & β’ β = (-gβπΊ) & β’ π· = (distβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = (πβ(π΅ β π΄))) | ||
Theorem | ngpds2 23884 | Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ β = (-gβπΊ) & β’ π· = (distβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = ((π΄ β π΅)π· 0 )) | ||
Theorem | ngpds2r 23885 | Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ β = (-gβπΊ) & β’ π· = (distβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = ((π΅ β π΄)π· 0 )) | ||
Theorem | ngpds3 23886 | Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ β = (-gβπΊ) & β’ π· = (distβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = ( 0 π·(π΄ β π΅))) | ||
Theorem | ngpds3r 23887 | Write the distance between two points in terms of distance from zero. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ β = (-gβπΊ) & β’ π· = (distβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = ( 0 π·(π΅ β π΄))) | ||
Theorem | ngprcan 23888 | Cancel right addition inside a distance calculation. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ π· = (distβπΊ) β β’ ((πΊ β NrmGrp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄ + πΆ)π·(π΅ + πΆ)) = (π΄π·π΅)) | ||
Theorem | ngplcan 23889 | Cancel left addition inside a distance calculation. (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ π· = (distβπΊ) β β’ (((πΊ β NrmGrp β§ πΊ β Abel) β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((πΆ + π΄)π·(πΆ + π΅)) = (π΄π·π΅)) | ||
Theorem | isngp4 23890* | Express the property of being a normed group purely in terms of right-translation invariance of the metric instead of using the definition of norm (which itself uses the metric). (Contributed by Mario Carneiro, 29-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ π· = (distβπΊ) β β’ (πΊ β NrmGrp β (πΊ β Grp β§ πΊ β MetSp β§ βπ₯ β π βπ¦ β π βπ§ β π ((π₯ + π§)π·(π¦ + π§)) = (π₯π·π¦))) | ||
Theorem | ngpinvds 23891 | Two elements are the same distance apart as their inverses. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ πΌ = (invgβπΊ) & β’ π· = (distβπΊ) β β’ (((πΊ β NrmGrp β§ πΊ β Abel) β§ (π΄ β π β§ π΅ β π)) β ((πΌβπ΄)π·(πΌβπ΅)) = (π΄π·π΅)) | ||
Theorem | ngpsubcan 23892 | Cancel right subtraction inside a distance calculation. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ β = (-gβπΊ) & β’ π· = (distβπΊ) β β’ ((πΊ β NrmGrp β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄ β πΆ)π·(π΅ β πΆ)) = (π΄π·π΅)) | ||
Theorem | nmf 23893 | The norm on a normed group is a function into the reals. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) β β’ (πΊ β NrmGrp β π:πβΆβ) | ||
Theorem | nmcl 23894 | The norm of a normed group is closed in the reals. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π) β (πβπ΄) β β) | ||
Theorem | nmge0 23895 | The norm of a normed group is nonnegative. Second part of Problem 2 of [Kreyszig] p. 64. (Contributed by NM, 28-Nov-2006.) (Revised by Mario Carneiro, 4-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π) β 0 β€ (πβπ΄)) | ||
Theorem | nmeq0 23896 | The identity is the only element of the group with zero norm. First part of Problem 2 of [Kreyszig] p. 64. (Contributed by NM, 24-Nov-2006.) (Revised by Mario Carneiro, 4-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π) β ((πβπ΄) = 0 β π΄ = 0 )) | ||
Theorem | nmne0 23897 | The norm of a nonzero element is nonzero. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π β§ π΄ β 0 ) β (πβπ΄) β 0) | ||
Theorem | nmrpcl 23898 | The norm of a nonzero element is a positive real. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π β§ π΄ β 0 ) β (πβπ΄) β β+) | ||
Theorem | nminv 23899 | The norm of a negated element is the same as the norm of the original element. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) & β’ πΌ = (invgβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π) β (πβ(πΌβπ΄)) = (πβπ΄)) | ||
Theorem | nmmtri 23900 | The triangle inequality for the norm of a subtraction. (Contributed by NM, 27-Dec-2007.) (Revised by Mario Carneiro, 4-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ π = (normβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β NrmGrp β§ π΄ β π β§ π΅ β π) β (πβ(π΄ β π΅)) β€ ((πβπ΄) + (πβπ΅))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |