Home | Metamath
Proof Explorer Theorem List (p. 223 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | xblpnf 22201 | The infinity ball in an extended metric is the set of all points that are a finite distance from the center. (Contributed by Mario Carneiro, 23-Aug-2015.) |
Theorem | blpnf 22202 | The infinity ball in a standard metric is just the whole space. (Contributed by Mario Carneiro, 23-Aug-2015.) |
Theorem | bldisj 22203 | Two balls are disjoint if the center-to-center distance is more than the sum of the radii. (Contributed by Mario Carneiro, 30-Dec-2013.) |
Theorem | blgt0 22204 | A nonempty ball implies that the radius is positive. (Contributed by NM, 11-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) |
Theorem | bl2in 22205 | Two balls are disjoint if they don't overlap. (Contributed by NM, 11-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) |
Theorem | xblss2ps 22206 | One ball is contained in another if the center-to-center distance is less than the difference of the radii. In this version of blss2 22209 for extended metrics, we have to assume the balls are a finite distance apart, or else will not even be in the infinity ball around . (Contributed by Mario Carneiro, 23-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
Theorem | xblss2 22207 | One ball is contained in another if the center-to-center distance is less than the difference of the radii. In this version of blss2 22209 for extended metrics, we have to assume the balls are a finite distance apart, or else will not even be in the infinity ball around . (Contributed by Mario Carneiro, 23-Aug-2015.) |
Theorem | blss2ps 22208 | One ball is contained in another if the center-to-center distance is less than the difference of the radii. (Contributed by Mario Carneiro, 15-Jan-2014.) (Revised by Mario Carneiro, 23-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
Theorem | blss2 22209 | One ball is contained in another if the center-to-center distance is less than the difference of the radii. (Contributed by Mario Carneiro, 15-Jan-2014.) (Revised by Mario Carneiro, 23-Aug-2015.) |
Theorem | blhalf 22210 | A ball of radius is contained in a ball of radius centered at any point inside the smaller ball. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Jan-2014.) |
Theorem | blfps 22211 | Mapping of a ball. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
Theorem | blf 22212 | Mapping of a ball. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) |
Theorem | blrnps 22213* | Membership in the range of the ball function. Note that is the collection of all balls for metric . (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
Theorem | blrn 22214* | Membership in the range of the ball function. Note that is the collection of all balls for metric . (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
Theorem | xblcntrps 22215 | A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
Theorem | xblcntr 22216 | A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
Theorem | blcntrps 22217 | A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
Theorem | blcntr 22218 | A ball contains its center. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
Theorem | xbln0 22219 | A ball is nonempty iff the radius is positive. (Contributed by Mario Carneiro, 23-Aug-2015.) |
Theorem | bln0 22220 | A ball is not empty. (Contributed by NM, 6-Oct-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) |
Theorem | blelrnps 22221 | A ball belongs to the set of balls of a metric space. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
Theorem | blelrn 22222 | A ball belongs to the set of balls of a metric space. (Contributed by NM, 2-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
Theorem | blssm 22223 | A ball is a subset of the base set of a metric space. (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
Theorem | unirnblps 22224 | The union of the set of balls of a metric space is its base set. (Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
Theorem | unirnbl 22225 | The union of the set of balls of a metric space is its base set. (Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
Theorem | blin 22226 | The intersection of two balls with the same center is the smaller of them. (Contributed by NM, 1-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
Theorem | ssblps 22227 | The size of a ball increases monotonically with its radius. (Contributed by NM, 20-Sep-2007.) (Revised by Mario Carneiro, 24-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
Theorem | ssbl 22228 | The size of a ball increases monotonically with its radius. (Contributed by NM, 20-Sep-2007.) (Revised by Mario Carneiro, 24-Aug-2015.) |
Theorem | blssps 22229* | Any point in a ball can be centered in another ball that is a subset of . (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 24-Aug-2015.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
Theorem | blss 22230* | Any point in a ball can be centered in another ball that is a subset of . (Contributed by NM, 31-Aug-2006.) (Revised by Mario Carneiro, 24-Aug-2015.) |
Theorem | blssexps 22231* | Two ways to express the existence of a ball subset. (Contributed by NM, 5-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) (Revised by Thierry Arnoux, 11-Mar-2018.) |
PsMet | ||
Theorem | blssex 22232* | Two ways to express the existence of a ball subset. (Contributed by NM, 5-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) |
Theorem | ssblex 22233* | A nested ball exists whose radius is less than any desired amount. (Contributed by NM, 20-Sep-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) |
Theorem | blin2 22234* | Given any two balls and a point in their intersection, there is a ball contained in the intersection with the given center point. (Contributed by Mario Carneiro, 12-Nov-2013.) |
Theorem | blbas 22235 | The balls of a metric space form a basis for a topology. (Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro, 15-Jan-2014.) |
Theorem | blres 22236 | A ball in a restricted metric space. (Contributed by Mario Carneiro, 5-Jan-2014.) |
Theorem | xmeterval 22237 | Value of the "finitely separated" relation. (Contributed by Mario Carneiro, 24-Aug-2015.) |
Theorem | xmeter 22238 | The "finitely separated" relation is an equivalence relation. (Contributed by Mario Carneiro, 24-Aug-2015.) |
Theorem | xmetec 22239 | The equivalence classes under the finite separation equivalence relation are infinity balls. Thus, by erdisj 7794, infinity balls are either identical or disjoint, quite unlike the usual situation with Euclidean balls which admit many kinds of overlap. (Contributed by Mario Carneiro, 24-Aug-2015.) |
Theorem | blssec 22240 | A ball centered at is contained in the set of points finitely separated from . This is just an application of ssbl 22228 to the infinity ball. (Contributed by Mario Carneiro, 24-Aug-2015.) |
Theorem | blpnfctr 22241 | The infinity ball in an extended metric acts like an ultrametric ball in that every point in the ball is also its center. (Contributed by Mario Carneiro, 21-Aug-2015.) |
Theorem | xmetresbl 22242 | An extended metric restricted to any ball (in particular the infinity ball) is a proper metric. Together with xmetec 22239, this shows that any extended metric space can be "factored" into the disjoint union of proper metric spaces, with points in the same region measured by that region's metric, and points in different regions being distance from each other. (Contributed by Mario Carneiro, 23-Aug-2015.) |
Theorem | mopnval 22243 | 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 22245, the open sets of a metric space form a topology , whose base set is by mopnuni 22246. (Contributed by NM, 1-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
Theorem | mopntopon 22244 | 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 | ||
Theorem | mopntop 22245 | 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.) |
Theorem | mopnuni 22246 | 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.) |
Theorem | elmopn 22247* | The defining property of an open set of a metric space. (Contributed by NM, 1-Sep-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
Theorem | mopnfss 22248 | 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.) |
Theorem | mopnm 22249 | 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.) |
Theorem | elmopn2 22250* | A defining property of an open set of a metric space. (Contributed by NM, 5-May-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) |
Theorem | mopnss 22251 | An open set of a metric space is a subspace of its base set. (Contributed by NM, 3-Sep-2006.) |
Theorem | isxms 22252 | Express the predicate " is an extended metric space" with underlying set and distance function . (Contributed by Mario Carneiro, 2-Sep-2015.) |
Theorem | isxms2 22253 | Express the predicate " is an extended metric space" with underlying set and distance function . (Contributed by Mario Carneiro, 2-Sep-2015.) |
Theorem | isms 22254 | 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.) |
Theorem | isms2 22255 | 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.) |
Theorem | xmstopn 22256 | The topology component of a metric space coincides with the topology generated by the metric component. (Contributed by Mario Carneiro, 26-Aug-2015.) |
Theorem | mstopn 22257 | The topology component of a metric space coincides with the topology generated by the metric component. (Contributed by Mario Carneiro, 26-Aug-2015.) |
Theorem | xmstps 22258 | A metric space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
Theorem | msxms 22259 | A metric space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
Theorem | mstps 22260 | A metric space is a topological space. (Contributed by Mario Carneiro, 26-Aug-2015.) |
Theorem | xmsxmet 22261 | The distance function, suitably truncated, is a metric on . (Contributed by Mario Carneiro, 2-Sep-2015.) |
Theorem | msmet 22262 | The distance function, suitably truncated, is a metric on . (Contributed by Mario Carneiro, 12-Nov-2013.) |
Theorem | msf 22263 | Mapping of the distance function of a metric space. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 12-Nov-2013.) |
Theorem | xmsxmet2 22264 | The distance function, suitably truncated, is a metric on . (Contributed by Mario Carneiro, 2-Oct-2015.) |
Theorem | msmet2 22265 | The distance function, suitably truncated, is a metric on . (Contributed by Mario Carneiro, 2-Oct-2015.) |
Theorem | mscl 22266 | Closure of the distance function of a metric space. (Contributed by NM, 30-Aug-2006.) (Revised by Mario Carneiro, 2-Oct-2015.) |
Theorem | xmscl 22267 | Closure of the distance function of an extended metric space. (Contributed by Mario Carneiro, 2-Oct-2015.) |
Theorem | xmsge0 22268 | The distance function in an extended metric space is nonnegative. (Contributed by Mario Carneiro, 4-Oct-2015.) |
Theorem | xmseq0 22269 | The distance function in an extended metric space is symmetric. (Contributed by Mario Carneiro, 2-Oct-2015.) |
Theorem | xmssym 22270 | The distance function in an extended metric space is symmetric. (Contributed by Mario Carneiro, 2-Oct-2015.) |
Theorem | xmstri2 22271 | Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 2-Oct-2015.) |
Theorem | mstri2 22272 | Triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.) |
Theorem | xmstri 22273 | 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.) |
Theorem | mstri 22274 | 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.) |
Theorem | xmstri3 22275 | Triangle inequality for the distance function of an extended metric. (Contributed by Mario Carneiro, 2-Oct-2015.) |
Theorem | mstri3 22276 | Triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 2-Oct-2015.) |
Theorem | msrtri 22277 | Reverse triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
Theorem | xmspropd 22278 | Property deduction for an extended metric space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
Theorem | mspropd 22279 | Property deduction for a metric space. (Contributed by Mario Carneiro, 4-Oct-2015.) |
Theorem | setsmsbas 22280 | The base set of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
sSet TopSet | ||
Theorem | setsmsds 22281 | The distance function of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
sSet TopSet | ||
Theorem | setsmstset 22282 | The topology of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
sSet TopSet TopSet | ||
Theorem | setsmstopn 22283 | The topology of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
sSet TopSet | ||
Theorem | setsxms 22284 | The constructed metric space is a metric space iff the provided distance function is a metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
sSet TopSet | ||
Theorem | setsms 22285 | The constructed metric space is a metric space iff the provided distance function is a metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
sSet TopSet | ||
Theorem | tmsval 22286 | For any metric there is an associated metric space. (Contributed by Mario Carneiro, 2-Sep-2015.) |
toMetSp sSet TopSet | ||
Theorem | tmslem 22287 | Lemma for tmsbas 22288, tmsds 22289, and tmstopn 22290. (Contributed by Mario Carneiro, 2-Sep-2015.) |
toMetSp | ||
Theorem | tmsbas 22288 | The base set of a constructed metric space. (Contributed by Mario Carneiro, 2-Sep-2015.) |
toMetSp | ||
Theorem | tmsds 22289 | The metric of a constructed metric space. (Contributed by Mario Carneiro, 2-Sep-2015.) |
toMetSp | ||
Theorem | tmstopn 22290 | The topology of a constructed metric. (Contributed by Mario Carneiro, 2-Sep-2015.) |
toMetSp | ||
Theorem | tmsxms 22291 | The constructed metric space is an extended metric space. (Contributed by Mario Carneiro, 2-Sep-2015.) |
toMetSp | ||
Theorem | tmsms 22292 | The constructed metric space is a metric space given a metric. (Contributed by Mario Carneiro, 2-Sep-2015.) |
toMetSp | ||
Theorem | imasf1obl 22293 | The image of a metric space ball. (Contributed by Mario Carneiro, 28-Aug-2015.) |
s | ||
Theorem | imasf1oxms 22294 | The image of a metric space is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
s | ||
Theorem | imasf1oms 22295 | The image of a metric space is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
s | ||
Theorem | prdsbl 22296* |
A ball in the product metric for finite index set is the Cartesian
product of balls in all coordinates. For infinite index set this is no
longer true; instead the correct statement is that a *closed ball* is
the product of closed balls in each coordinate (where closed ball means
a set of the form in blcld 22310) - for a counterexample the point in
whose -th coordinate is is in
but is not in
the -ball of the
product (since ).
The last assumption, , is needed only in the case , when the right side evaluates to and the left evaluates to if and if . (Contributed by Mario Carneiro, 28-Aug-2015.) |
s | ||
Theorem | mopni 22297* | 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.) |
Theorem | mopni2 22298* | 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.) |
Theorem | mopni3 22299* | 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.) |
Theorem | blssopn 22300 | The balls of a metric space are open sets. (Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro, 23-Dec-2013.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |