Home | Metamath
Proof Explorer Theorem List (p. 227 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 | blcvx 22601 | An open ball in the complex numbers is a convex set. (Contributed by Mario Carneiro, 12-Feb-2015.) (Revised by Mario Carneiro, 8-Sep-2015.) |
Theorem | rehaus 22602 | The standard topology on the reals is Hausdorff. (Contributed by NM, 8-Mar-2007.) |
Theorem | tgqioo 22603 | The topology generated by open intervals of reals with rational endpoints is the same as the open sets of the standard metric space on the reals. In particular, this proves that the standard topology on the reals is second-countable. (Contributed by Mario Carneiro, 17-Jun-2014.) |
Theorem | re2ndc 22604 | The standard topology on the reals is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
Theorem | resubmet 22605 | The subspace topology induced by a subset of the reals. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Aug-2014.) |
↾t | ||
Theorem | tgioo2 22606 | The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014.) |
ℂfld ↾t | ||
Theorem | rerest 22607 | The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 13-Aug-2014.) |
ℂfld ↾t ↾t | ||
Theorem | tgioo3 22608 | The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by Thierry Arnoux, 3-Jul-2019.) |
RRfld | ||
Theorem | xrtgioo 22609 | The topology on the extended reals coincides with the standard topology on the reals, when restricted to . (Contributed by Mario Carneiro, 3-Sep-2015.) |
ordTop ↾t | ||
Theorem | xrrest 22610 | The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 9-Sep-2015.) |
ordTop ↾t ↾t | ||
Theorem | xrrest2 22611 | The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 9-Sep-2015.) |
ℂfld ordTop ↾t ↾t | ||
Theorem | xrsxmet 22612 | The metric on the extended reals is a proper extended metric. (Contributed by Mario Carneiro, 4-Sep-2015.) |
Theorem | xrsdsre 22613 | The metric on the extended reals coincides with the usual metric on the reals. (Contributed by Mario Carneiro, 4-Sep-2015.) |
Theorem | xrsblre 22614 | Any ball of the metric of the extended reals centered on an element of is entirely contained in . (Contributed by Mario Carneiro, 4-Sep-2015.) |
Theorem | xrsmopn 22615 | The metric on the extended reals generates a topology, but this does not match the order topology on ; for example is open in the metric topology, but not the order topology. However, the metric topology is finer than the order topology, meaning that all open intervals are open in the metric topology. (Contributed by Mario Carneiro, 4-Sep-2015.) |
ordTop | ||
Theorem | zcld 22616 | The integers are a closed set in the topology on . (Contributed by Mario Carneiro, 17-Feb-2015.) |
Theorem | recld2 22617 | The real numbers are a closed set in the topology on . (Contributed by Mario Carneiro, 17-Feb-2015.) |
ℂfld | ||
Theorem | zcld2 22618 | The integers are a closed set in the topology on . (Contributed by Mario Carneiro, 17-Feb-2015.) |
ℂfld | ||
Theorem | zdis 22619 | The integers are a discrete set in the topology on . (Contributed by Mario Carneiro, 19-Sep-2015.) |
ℂfld ↾t | ||
Theorem | sszcld 22620 | Every subset of the integers are closed in the topology on . (Contributed by Mario Carneiro, 6-Jul-2017.) |
ℂfld | ||
Theorem | reperflem 22621* | A subset of the real numbers that is closed under addition with real numbers is perfect. (Contributed by Mario Carneiro, 26-Dec-2016.) |
ℂfld ↾t Perf | ||
Theorem | reperf 22622 | The real numbers are a perfect subset of the complex numbers. (Contributed by Mario Carneiro, 26-Dec-2016.) |
ℂfld ↾t Perf | ||
Theorem | cnperf 22623 | The complex numbers are a perfect space. (Contributed by Mario Carneiro, 26-Dec-2016.) |
ℂfld Perf | ||
Theorem | iccntr 22624 | The interior of a closed interval in the standard topology on is the corresponding open interval. (Contributed by Mario Carneiro, 1-Sep-2014.) |
Theorem | icccmplem1 22625* | Lemma for icccmp 22628. (Contributed by Mario Carneiro, 18-Jun-2014.) |
↾t | ||
Theorem | icccmplem2 22626* | Lemma for icccmp 22628. (Contributed by Mario Carneiro, 13-Jun-2014.) |
↾t | ||
Theorem | icccmplem3 22627* | Lemma for icccmp 22628. (Contributed by Mario Carneiro, 13-Jun-2014.) |
↾t | ||
Theorem | icccmp 22628 | A closed interval in is compact. (Contributed by Mario Carneiro, 13-Jun-2014.) |
↾t | ||
Theorem | reconnlem1 22629 | Lemma for reconn 22631. Connectedness in the reals-easy direction. (Contributed by Jeff Hankins, 13-Jul-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.) |
↾t Conn | ||
Theorem | reconnlem2 22630* | Lemma for reconn 22631. (Contributed by Jeff Hankins, 17-Aug-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.) |
Theorem | reconn 22631* | A subset of the reals is connected iff it has the interval property. (Contributed by Jeff Hankins, 15-Jul-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.) |
↾t Conn | ||
Theorem | retopconn 22632 | Corollary of reconn 22631. The set of real numbers is connected. (Contributed by Jeff Hankins, 17-Aug-2009.) |
Conn | ||
Theorem | iccconn 22633 | A closed interval is connected. (Contributed by Jeff Hankins, 17-Aug-2009.) |
↾t Conn | ||
Theorem | opnreen 22634 | Every nonempty open set is uncountable. (Contributed by Mario Carneiro, 26-Jul-2014.) (Revised by Mario Carneiro, 20-Feb-2015.) |
Theorem | rectbntr0 22635 | A countable subset of the reals has empty interior. (Contributed by Mario Carneiro, 26-Jul-2014.) |
Theorem | xrge0gsumle 22636 | A finite sum in the nonnegative extended reals is monotonic in the support. (Contributed by Mario Carneiro, 13-Sep-2015.) |
↾s g g | ||
Theorem | xrge0tsms 22637* | Any finite or infinite sum in the nonnegative extended reals is uniquely convergent to the supremum of all finite sums. (Contributed by Mario Carneiro, 13-Sep-2015.) (Proof shortened by AV, 26-Jul-2019.) |
↾s g tsums | ||
Theorem | xrge0tsms2 22638 | Any finite or infinite sum in the nonnegative extended reals is convergent. This is a rather unique property of the set ; a similar theorem is not true for or or . It is true for , however, or more generally any additive submonoid of with adjoined. (Contributed by Mario Carneiro, 13-Sep-2015.) |
↾s tsums | ||
Theorem | metdcnlem 22639 | The metric function of a metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 4-Sep-2015.) |
Theorem | xmetdcn2 22640 | The metric function of an extended metric space is always continuous in the topology generated by it. In this variation of xmetdcn 22641 we use the metric topology instead of the order topology on , which makes the theorem a bit stronger. Since is an isolated point in the metric topology, this is saying that for any points which are an infinite distance apart, there is a product neighborhood around such that for any near and near , i.e. the distance function is locally constant . (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 4-Sep-2015.) |
Theorem | xmetdcn 22641 | The metric function of an extended metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 4-Sep-2015.) |
ordTop | ||
Theorem | metdcn2 22642 | The metric function of a metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 4-Sep-2015.) |
Theorem | metdcn 22643 | The metric function of a metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 4-Sep-2015.) |
ℂfld | ||
Theorem | msdcn 22644 | The metric function of a metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 5-Oct-2015.) |
Theorem | cnmpt1ds 22645* | Continuity of the metric function; analogue of cnmpt12f 21469 which cannot be used directly because is not necessarily a function. (Contributed by Mario Carneiro, 5-Oct-2015.) |
TopOn | ||
Theorem | cnmpt2ds 22646* | Continuity of the metric function; analogue of cnmpt22f 21478 which cannot be used directly because is not necessarily a function. (Contributed by Mario Carneiro, 5-Oct-2015.) |
TopOn TopOn | ||
Theorem | nmcn 22647 | The norm of a normed group is a continuous function. (Contributed by Mario Carneiro, 4-Oct-2015.) |
NrmGrp | ||
Theorem | ngnmcncn 22648 | The norm of a normed group is a continuous function to . (Contributed by NM, 12-Aug-2007.) (Revised by AV, 17-Oct-2021.) |
ℂfld NrmGrp | ||
Theorem | abscn 22649 | The absolute value function on complex numbers is continuous. (Contributed by NM, 22-Aug-2007.) (Proof shortened by Mario Carneiro, 10-Jan-2014.) |
ℂfld | ||
Theorem | metdsval 22650* | Value of the "distance to a set" function. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by Mario Carneiro, 4-Sep-2015.) (Revised by AV, 30-Sep-2020.) |
inf inf | ||
Theorem | metdsf 22651* | The distance from a point to a set is a nonnegative extended real number. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by Mario Carneiro, 4-Sep-2015.) (Proof shortened by AV, 30-Sep-2020.) |
inf | ||
Theorem | metdsge 22652* | The distance from the point to the set is greater than iff the -ball around misses . (Contributed by Mario Carneiro, 4-Sep-2015.) (Proof shortened by AV, 30-Sep-2020.) |
inf | ||
Theorem | metds0 22653* | If a point is in a set, its distance to the set is zero. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by Mario Carneiro, 4-Sep-2015.) |
inf | ||
Theorem | metdstri 22654* | A generalization of the triangle inequality to the point-set distance function. Under the usual notation where the same symbol denotes the point-point and point-set distance functions, this theorem would be written . (Contributed by Mario Carneiro, 4-Sep-2015.) |
inf | ||
Theorem | metdsle 22655* | The distance from a point to a set is bounded by the distance to any member of the set. (Contributed by Mario Carneiro, 5-Sep-2015.) |
inf | ||
Theorem | metdsre 22656* | The distance from a point to a nonempty set in a proper metric space is a real number. (Contributed by Mario Carneiro, 5-Sep-2015.) |
inf | ||
Theorem | metdseq0 22657* | The distance from a point to a set is zero iff the point is in the closure set. (Contributed by Mario Carneiro, 14-Feb-2015.) |
inf | ||
Theorem | metdscnlem 22658* | Lemma for metdscn 22659. (Contributed by Mario Carneiro, 4-Sep-2015.) |
inf | ||
Theorem | metdscn 22659* | The function which gives the distance from a point to a set is a continuous function into the metric topology of the extended reals. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by Mario Carneiro, 4-Sep-2015.) |
inf | ||
Theorem | metdscn2 22660* | The function which gives the distance from a point to a nonempty set in a metric space is a continuous function into the topology of the complex numbers. (Contributed by Mario Carneiro, 5-Sep-2015.) |
inf ℂfld | ||
Theorem | metnrmlem1a 22661* | Lemma for metnrm 22665. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Mario Carneiro, 4-Sep-2015.) |
inf | ||
Theorem | metnrmlem1 22662* | Lemma for metnrm 22665. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Mario Carneiro, 4-Sep-2015.) |
inf | ||
Theorem | metnrmlem2 22663* | Lemma for metnrm 22665. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Mario Carneiro, 5-Sep-2015.) |
inf | ||
Theorem | metnrmlem3 22664* | Lemma for metnrm 22665. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Mario Carneiro, 5-Sep-2015.) |
inf inf | ||
Theorem | metnrm 22665 | A metric space is normal. (Contributed by Jeff Hankins, 31-Aug-2013.) (Revised by Mario Carneiro, 5-Sep-2015.) (Proof shortened by AV, 30-Sep-2020.) |
Theorem | metreg 22666 | A metric space is regular. (Contributed by Mario Carneiro, 29-Dec-2016.) |
Theorem | addcnlem 22667* | Lemma for addcn 22668, subcn 22669, and mulcn 22670. (Contributed by Mario Carneiro, 5-May-2014.) (Proof shortened by Mario Carneiro, 2-Sep-2015.) |
ℂfld | ||
Theorem | addcn 22668 | Complex number addition is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by NM, 30-Jul-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.) |
ℂfld | ||
Theorem | subcn 22669 | Complex number subtraction is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by NM, 4-Aug-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.) |
ℂfld | ||
Theorem | mulcn 22670 | Complex number multiplication is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by NM, 30-Jul-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.) |
ℂfld | ||
Theorem | divcn 22671 | Complex number division is a continuous function, when the second argument is nonzero. (Contributed by Mario Carneiro, 12-Aug-2014.) |
ℂfld ↾t | ||
Theorem | cnfldtgp 22672 | The complex numbers form a topological group under addition, with the standard topology induced by the absolute value metric. (Contributed by Mario Carneiro, 2-Sep-2015.) |
ℂfld | ||
Theorem | fsumcn 22673* | A finite sum of functions to complex numbers from a common topological space is continuous. The class expression for normally contains free variables and to index it. (Contributed by NM, 8-Aug-2007.) (Revised by Mario Carneiro, 23-Aug-2014.) |
ℂfld TopOn | ||
Theorem | fsum2cn 22674* | Version of fsumcn 22673 for two-argument mappings. (Contributed by Mario Carneiro, 6-May-2014.) |
ℂfld TopOn TopOn | ||
Theorem | expcn 22675* | The power function on complex numbers, for fixed exponent , is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) |
ℂfld | ||
Theorem | divccn 22676* | Division by a nonzero constant is a continuous operation. (Contributed by Mario Carneiro, 5-May-2014.) |
ℂfld | ||
Theorem | sqcn 22677* | The square function on complex numbers is continuous. (Contributed by NM, 13-Jun-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.) |
ℂfld | ||
Syntax | cii 22678 | Extend class notation with the unit interval. |
Syntax | ccncf 22679 | Extend class notation to include the operation which returns a class of continuous complex functions. |
Definition | df-ii 22680 | Define the unit interval with the Euclidean topology. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 3-Sep-2015.) |
Definition | df-cncf 22681* | Define the operation whose value is a class of continuous complex functions. (Contributed by Paul Chapman, 11-Oct-2007.) |
Theorem | iitopon 22682 | The unit interval is a topological space. (Contributed by Mario Carneiro, 3-Sep-2015.) |
TopOn | ||
Theorem | iitop 22683 | The unit interval is a topological space. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | iiuni 22684 | The base set of the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Jan-2014.) |
Theorem | dfii2 22685 | Alternate definition of the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
↾t | ||
Theorem | dfii3 22686 | Alternate definition of the unit interval. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 3-Sep-2015.) |
ℂfld ↾t | ||
Theorem | dfii4 22687 | Alternate definition of the unit interval. (Contributed by Mario Carneiro, 3-Sep-2015.) |
ℂfld ↾s | ||
Theorem | dfii5 22688 | The unit interval expressed as an order topology. (Contributed by Mario Carneiro, 9-Sep-2015.) |
ordTop | ||
Theorem | iicmp 22689 | The unit interval is compact. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Jun-2014.) |
Theorem | iiconn 22690 | The unit interval is connected. (Contributed by Mario Carneiro, 11-Feb-2015.) |
Conn | ||
Theorem | cncfval 22691* | The value of the continuous complex function operation is the set of continuous functions from to . (Contributed by Paul Chapman, 11-Oct-2007.) (Revised by Mario Carneiro, 9-Nov-2013.) |
Theorem | elcncf 22692* | Membership in the set of continuous complex functions from to . (Contributed by Paul Chapman, 11-Oct-2007.) (Revised by Mario Carneiro, 9-Nov-2013.) |
Theorem | elcncf2 22693* | Version of elcncf 22692 with arguments commuted. (Contributed by Mario Carneiro, 28-Apr-2014.) |
Theorem | cncfrss 22694 | Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.) |
Theorem | cncfrss2 22695 | Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.) |
Theorem | cncff 22696 | A continuous complex function's domain and codomain. (Contributed by Paul Chapman, 17-Jan-2008.) (Revised by Mario Carneiro, 25-Aug-2014.) |
Theorem | cncfi 22697* | Defining property of a continuous function. (Contributed by Mario Carneiro, 30-Apr-2014.) (Revised by Mario Carneiro, 25-Aug-2014.) |
Theorem | elcncf1di 22698* | Membership in the set of continuous complex functions from to . (Contributed by Paul Chapman, 26-Nov-2007.) |
Theorem | elcncf1ii 22699* | Membership in the set of continuous complex functions from to . (Contributed by Paul Chapman, 26-Nov-2007.) |
Theorem | rescncf 22700 | A continuous complex function restricted to a subset is continuous. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 25-Aug-2014.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |