HomeTheorem List (p. 149 of 159)
Unicode version.
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Intuitionistic Logic Explorer Theorem List (p. 149 of 159) | < Previous Next > |
| Browser slow? Try the
Unicode version. |
||
|
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | setsmstsetg 14801 | The topology of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) (Revised by Jim Kingdon, 7-May-2023.) |
              
sSet  TopSet 
 
    TopSet | ||
| Theorem | mopni 14802* | 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.) |
   ![/\](wedge.gif "/\"){kind=small}      
 | ||
| Theorem | mopni2 14803* | 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 14804* | 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 14805 | The balls of a metric space are open sets. (Contributed by NM, 12-Sep-2006.) (Revised by Mario Carneiro, 23-Dec-2013.) |
| | ||
| Theorem | unimopn 14806 | 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.) |
 | ||
| Theorem | mopnin 14807 | 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.) |
 
| ||
| Theorem | mopn0 14808 | 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.) |
| ||
| Theorem | rnblopn 14809 | A ball of a metric space is an open set. (Contributed by NM, 12-Sep-2006.) |
|
| ||
| Theorem | blopn 14810 | A ball of a metric space is an open set. (Contributed by NM, 9-Mar-2007.) (Revised by Mario Carneiro, 12-Nov-2013.) |
 | ||
| Theorem | neibl 14811* |
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.)
|
      | ||
| Theorem | blnei 14812 | A ball around a point is a neighborhood of the point. (Contributed by NM, 8-Nov-2007.) (Revised by Mario Carneiro, 24-Aug-2015.) |
| | ||
| Theorem | blsscls2 14813* | A smaller closed ball is contained in a larger open ball. (Contributed by Mario Carneiro, 10-Jan-2014.) |
   
| ||
| Theorem | metss 14814* |
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.)
|
 
| ||
| Theorem | metequiv 14815* | 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.) |
 
| ||
| Theorem | metequiv2 14816* | 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.) |
|
| ||
| Theorem | metss2lem 14817* | Lemma for metss2 14818. (Contributed by Mario Carneiro, 14-Sep-2015.) |
 | ||
| Theorem | metss2 14818* |
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.)
|
|
| ||
| Theorem | comet 14819* | The composition of an extended metric with a monotonic subadditive function is an extended metric. (Contributed by Mario Carneiro, 21-Mar-2015.) |
   ![[,]](_icc.gif "[,]"){kind=small}  
 
 | ||
| Theorem | bdmetval 14820* | Value of the standard bounded metric. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 9-May-2023.) |
 inf
inf
| ||
| Theorem | bdxmet 14821* | 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
| ||
| Theorem | bdmet 14822* | 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 | ||
| Theorem | bdbl 14823* |
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
| ||
| Theorem | bdmopn 14824* |
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 | ||
| Theorem | mopnex 14825* | 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.) |
 | ||
| Theorem | metrest 14826 | 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 | ||
| Theorem | xmetxp 14827* | The maximum metric (Chebyshev distance) on the product of two sets. (Contributed by Jim Kingdon, 11-Oct-2023.) |
    
| ||
| Theorem | xmetxpbl 14828* |
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.)
|
|
| ||
| Theorem | xmettxlem 14829* | Lemma for xmettx 14830. (Contributed by Jim Kingdon, 15-Oct-2023.) |
  | ||
| Theorem | xmettx 14830* | The maximum metric (Chebyshev distance) on the product of two sets, expressed as a binary topological product. (Contributed by Jim Kingdon, 11-Oct-2023.) |
|
| ||
| Theorem | metcnp3 14831* |
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.)
|
  | ||
| Theorem | metcnp 14832* |
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.)
|
 | ||
| Theorem | metcnp2 14833* |
Two ways to say a mapping from metric to metric is
continuous at point . The distance arguments are swapped compared
to metcnp 14832 (and Munkres' metcn 14834) for compatibility with df-lm 14510.
Definition 1.3-3 of [Kreyszig] p. 20.
(Contributed by NM, 4-Jun-2007.)
(Revised by Mario Carneiro, 13-Nov-2013.)
|
| | ||
| Theorem | metcn 14834* |
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.)
|
| ||
| Theorem | metcnpi 14835* | Epsilon-delta property of a continuous metric space function, with function arguments as in metcnp 14832. (Contributed by NM, 17-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
|
| ||
| Theorem | metcnpi2 14836* | Epsilon-delta property of a continuous metric space function, with swapped distance function arguments as in metcnp2 14833. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
|
| ||
| Theorem | metcnpi3 14837* |
Epsilon-delta property of a metric space function continuous at .
A variation of metcnpi2 14836 with non-strict ordering. (Contributed by
NM,
16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|
|
| ||
| Theorem | txmetcnp 14838* | Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.) (Revised by Jim Kingdon, 22-Oct-2023.) |
 
| ||
| Theorem | txmetcn 14839* | Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.) |
|
| ||
| Theorem | metcnpd 14840* |
Two ways to say a mapping from metric to metric is
continuous at point . (Contributed by Jim Kingdon,
14-Jun-2023.)
|
|
| ||
| Theorem | qtopbasss 14841* | 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
  | ||
| Theorem | qtopbas 14842 | The set of open intervals with rational endpoints forms a basis for a topology. (Contributed by NM, 8-Mar-2007.) |
 | ||
| Theorem | retopbas 14843 | A basis for the standard topology on the reals. (Contributed by NM, 6-Feb-2007.) (Proof shortened by Mario Carneiro, 17-Jun-2014.) |
| | ||
| Theorem | retop 14844 | The standard topology on the reals. (Contributed by FL, 4-Jun-2007.) |
  | ||
| Theorem | uniretop 14845 | The underlying set of the standard topology on the reals is the reals. (Contributed by FL, 4-Jun-2007.) |
| ||
| Theorem | retopon 14846 | The standard topology on the reals is a topology on the reals. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| TopOn | ||
| Theorem | retps 14847 | The standard topological space on the reals. (Contributed by NM, 19-Oct-2012.) |
TopSet
 | ||
| Theorem | iooretopg 14848 | 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.) |
|
| ||
| Theorem | cnmetdval 14849 | 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.) |
 
 | ||
| Theorem | cnmet 14850 | 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.) |
|
| ||
| Theorem | cnxmet 14851 | The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
|
| ||
| Theorem | cntoptopon 14852 | The topology of the complex numbers is a topology. (Contributed by Jim Kingdon, 6-Jun-2023.) |
| TopOn | ||
| Theorem | cntoptop 14853 | The topology of the complex numbers is a topology. (Contributed by Jim Kingdon, 6-Jun-2023.) |
| | ||
| Theorem | cnbl0 14854 | Two ways to write the open ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.) |
  | ||
| Theorem | cnblcld 14855* | Two ways to write the closed ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.) |
|
| ||
| Theorem | cnfldms 14856 | The complex number field is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
ℂfld  | ||
| Theorem | cnfldxms 14857 | The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ℂfld | ||
| Theorem | cnfldtps 14858 | The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ℂfld | ||
| Theorem | cnfldtopn 14859 | The topology of the complex numbers. (Contributed by Mario Carneiro, 28-Aug-2015.) |
 ℂfld | ||
| Theorem | cnfldtopon 14860 | The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ℂfld TopOn | ||
| Theorem | cnfldtop 14861 | The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ℂfld | ||
| Theorem | unicntopcntop 14862 | 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.) |
| | ||
| Theorem | unicntop 14863 | The underlying set of the standard topology on the complex numbers is the set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ℂfld | ||
| Theorem | cnopncntop 14864 | 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.) |
|
| ||
| Theorem | cnopn 14865 | The set of complex numbers is open with respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
|
ℂfld | ||
| Theorem | reopnap 14866* | The real numbers apart from a given real number form an open set. (Contributed by Jim Kingdon, 13-Dec-2023.) |
| #
| ||
| Theorem | remetdval 14867 | Value of the distance function of the metric space of real numbers. (Contributed by NM, 16-May-2007.) |
|
| ||
| Theorem | remet 14868 | The absolute value metric determines a metric space on the reals. (Contributed by NM, 10-Feb-2007.) |
| | ||
| Theorem | rexmet 14869 | The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| | ||
| Theorem | bl2ioo 14870 | A ball in terms of an open interval of reals. (Contributed by NM, 18-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
| | ||
| Theorem | ioo2bl 14871 | An open interval of reals in terms of a ball. (Contributed by NM, 18-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.) |
 | ||
| Theorem | ioo2blex 14872 | An open interval of reals in terms of a ball. (Contributed by Mario Carneiro, 14-Nov-2013.) |
| | ||
| Theorem | blssioo 14873 | The balls of the standard real metric space are included in the open real intervals. (Contributed by NM, 8-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
|
| ||
| Theorem | tgioo 14874 | The topology generated by open intervals of reals is the same as the open sets of the standard metric space on the reals. (Contributed by NM, 7-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
| | ||
| Theorem | tgqioo 14875 | 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 | resubmet 14876 | 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 | tgioo2cntop 14877 | The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by Jim Kingdon, 6-Aug-2023.) |
|
↾t | ||
| Theorem | rerestcntop 14878 | The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by Jim Kingdon, 6-Aug-2023.) |
|
↾t ↾t | ||
| Theorem | tgioo2 14879 | 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 14880 | The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 13-Aug-2014.) |
| ℂfld ↾t
↾t | ||
| Theorem | addcncntoplem 14881* | Lemma for addcncntop 14882, subcncntop 14883, and mulcncntop 14884. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Jim Kingdon, 22-Oct-2023.) |
 
| ||
| Theorem | addcncntop 14882 | 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.) |
|
| ||
| Theorem | subcncntop 14883 | 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.) |
|
| ||
| Theorem | mulcncntop 14884 | 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.) |
|
| ||
| Theorem | divcnap 14885* | Complex number division is a continuous function, when the second argument is apart from zero. (Contributed by Mario Carneiro, 12-Aug-2014.) (Revised by Jim Kingdon, 25-Oct-2023.) |
| ↾t
#
#
| ||
| Theorem | mpomulcn 14886* | Complex number multiplication is a continuous function. (Contributed by GG, 16-Mar-2025.) |
| ℂfld
| ||
| Theorem | fsumcncntop 14887* |
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.)
|
TopOn 
| ||
| Theorem | fsumcn 14888* |
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 | expcn 14889* |
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.) Avoid ax-mulf 8019. (Revised by GG,
16-Mar-2025.)
|
ℂfld
 | ||
| Syntax | ccncf 14890 | Extend class notation to include the operation which returns a class of continuous complex functions. |
  | ||
| Definition | df-cncf 14891* | Define the operation whose value is a class of continuous complex functions. (Contributed by Paul Chapman, 11-Oct-2007.) |
  
 | ||
| Theorem | cncfval 14892* |
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 14893* |
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 14894* | Version of elcncf 14893 with arguments commuted. (Contributed by Mario Carneiro, 28-Apr-2014.) |
| | ||
| Theorem | cncfrss 14895 | Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.) |
| | ||
| Theorem | cncfrss2 14896 | Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.) |
| | ||
| Theorem | cncff 14897 | A continuous complex function's domain and codomain. (Contributed by Paul Chapman, 17-Jan-2008.) (Revised by Mario Carneiro, 25-Aug-2014.) |
| | ||
| Theorem | cncfi 14898* | Defining property of a continuous function. (Contributed by Mario Carneiro, 30-Apr-2014.) (Revised by Mario Carneiro, 25-Aug-2014.) |
|
| ||
| Theorem | elcncf1di 14899* |
Membership in the set of continuous complex functions from to
. (Contributed
by Paul Chapman, 26-Nov-2007.)
|
|
| ||
| Theorem | elcncf1ii 14900* |
Membership in the set of continuous complex functions from to
. (Contributed
by Paul Chapman, 26-Nov-2007.)
|
|
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |