HomeTheorem List (p. 153 of 167)
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. 153 of 167) | < 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 | mopnin 15201 | 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.) |
             ![/\](wedge.gif "/\"){kind=small}    
| ||
| Theorem | mopn0 15202 | 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 15203 | A ball of a metric space is an open set. (Contributed by NM, 12-Sep-2006.) |
 
| ||
| Theorem | blopn 15204 | 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 15205* |
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 15206 | 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 15207* | A smaller closed ball is contained in a larger open ball. (Contributed by Mario Carneiro, 10-Jan-2014.) |
    
 | ||
| Theorem | metss 15208* |
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 15209* | 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 15210* | 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 15211* | Lemma for metss2 15212. (Contributed by Mario Carneiro, 14-Sep-2015.) |
 | ||
| Theorem | metss2 15212* |
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 15213* | 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 15214* | Value of the standard bounded metric. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 9-May-2023.) |
 inf 
inf
| ||
| Theorem | bdxmet 15215* | 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 15216* | 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 15217* |
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 15218* |
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 15219* | 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 15220 | 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 15221* | The maximum metric (Chebyshev distance) on the product of two sets. (Contributed by Jim Kingdon, 11-Oct-2023.) |
     
| ||
| Theorem | xmetxpbl 15222* |
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 15223* | Lemma for xmettx 15224. (Contributed by Jim Kingdon, 15-Oct-2023.) |
  | ||
| Theorem | xmettx 15224* | 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 15225* |
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 15226* |
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 15227* |
Two ways to say a mapping from metric to metric is
continuous at point . The distance arguments are swapped compared
to metcnp 15226 (and Munkres' metcn 15228) for compatibility with df-lm 14904.
Definition 1.3-3 of [Kreyszig] p. 20.
(Contributed by NM, 4-Jun-2007.)
(Revised by Mario Carneiro, 13-Nov-2013.)
|
| | ||
| Theorem | metcn 15228* |
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 15229* | Epsilon-delta property of a continuous metric space function, with function arguments as in metcnp 15226. (Contributed by NM, 17-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
|
| ||
| Theorem | metcnpi2 15230* | Epsilon-delta property of a continuous metric space function, with swapped distance function arguments as in metcnp2 15227. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
|
| ||
| Theorem | metcnpi3 15231* |
Epsilon-delta property of a metric space function continuous at .
A variation of metcnpi2 15230 with non-strict ordering. (Contributed by
NM,
16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|
|
| ||
| Theorem | txmetcnp 15232* | Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.) (Revised by Jim Kingdon, 22-Oct-2023.) |
 
 
| ||
| Theorem | txmetcn 15233* | Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.) |
|
| ||
| Theorem | metcnpd 15234* |
Two ways to say a mapping from metric to metric is
continuous at point . (Contributed by Jim Kingdon,
14-Jun-2023.)
|
|
| ||
| Theorem | qtopbasss 15235* | 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 15236 | The set of open intervals with rational endpoints forms a basis for a topology. (Contributed by NM, 8-Mar-2007.) |
 | ||
| Theorem | retopbas 15237 | 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 15238 | The standard topology on the reals. (Contributed by FL, 4-Jun-2007.) |
  | ||
| Theorem | uniretop 15239 | The underlying set of the standard topology on the reals is the reals. (Contributed by FL, 4-Jun-2007.) |
 
| ||
| Theorem | retopon 15240 | The standard topology on the reals is a topology on the reals. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| TopOn | ||
| Theorem | retps 15241 | The standard topological space on the reals. (Contributed by NM, 19-Oct-2012.) |
  TopSet
 | ||
| Theorem | iooretopg 15242 | 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 15243 | 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 15244 | 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 15245 | The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
|
| ||
| Theorem | cntoptopon 15246 | The topology of the complex numbers is a topology. (Contributed by Jim Kingdon, 6-Jun-2023.) |
| TopOn | ||
| Theorem | cntoptop 15247 | The topology of the complex numbers is a topology. (Contributed by Jim Kingdon, 6-Jun-2023.) |
| | ||
| Theorem | cnbl0 15248 | Two ways to write the open ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.) |
  | ||
| Theorem | cnblcld 15249* | Two ways to write the closed ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.) |
|
| ||
| Theorem | cnfldms 15250 | The complex number field is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
ℂfld  | ||
| Theorem | cnfldxms 15251 | The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ℂfld | ||
| Theorem | cnfldtps 15252 | The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ℂfld | ||
| Theorem | cnfldtopn 15253 | The topology of the complex numbers. (Contributed by Mario Carneiro, 28-Aug-2015.) |
 ℂfld | ||
| Theorem | cnfldtopon 15254 | The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ℂfld TopOn | ||
| Theorem | cnfldtop 15255 | The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ℂfld | ||
| Theorem | unicntopcntop 15256 | 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 15257 | 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 15258 | 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 15259 | 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 15260* | The real numbers apart from a given real number form an open set. (Contributed by Jim Kingdon, 13-Dec-2023.) |
| #
| ||
| Theorem | remetdval 15261 | Value of the distance function of the metric space of real numbers. (Contributed by NM, 16-May-2007.) |
|
| ||
| Theorem | remet 15262 | The absolute value metric determines a metric space on the reals. (Contributed by NM, 10-Feb-2007.) |
| | ||
| Theorem | rexmet 15263 | The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| | ||
| Theorem | bl2ioo 15264 | 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 15265 | 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 15266 | An open interval of reals in terms of a ball. (Contributed by Mario Carneiro, 14-Nov-2013.) |
| | ||
| Theorem | blssioo 15267 | 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 15268 | 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 15269 | 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 15270 | 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 15271 | 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 15272 | 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 15273 | 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 15274 | The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 13-Aug-2014.) |
| ℂfld ↾t
↾t | ||
| Theorem | addcncntoplem 15275* | Lemma for addcncntop 15276, subcncntop 15277, and mulcncntop 15278. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Jim Kingdon, 22-Oct-2023.) |
 
| ||
| Theorem | addcncntop 15276 | 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 15277 | 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 15278 | 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 15279* | 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 15280* | Complex number multiplication is a continuous function. (Contributed by GG, 16-Mar-2025.) |
| ℂfld
| ||
| Theorem | fsumcncntop 15281* |
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 15282* |
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 15283* |
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 8145. (Revised by GG,
16-Mar-2025.)
|
ℂfld
 | ||
| Syntax | ccncf 15284 | Extend class notation to include the operation which returns a class of continuous complex functions. |
  | ||
| Definition | df-cncf 15285* | Define the operation whose value is a class of continuous complex functions. (Contributed by Paul Chapman, 11-Oct-2007.) |
  
 | ||
| Theorem | cncfval 15286* |
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 15287* |
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 15288* | Version of elcncf 15287 with arguments commuted. (Contributed by Mario Carneiro, 28-Apr-2014.) |
| | ||
| Theorem | cncfrss 15289 | Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.) |
| | ||
| Theorem | cncfrss2 15290 | Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.) |
| | ||
| Theorem | cncff 15291 | A continuous complex function's domain and codomain. (Contributed by Paul Chapman, 17-Jan-2008.) (Revised by Mario Carneiro, 25-Aug-2014.) |
| | ||
| Theorem | cncfi 15292* | Defining property of a continuous function. (Contributed by Mario Carneiro, 30-Apr-2014.) (Revised by Mario Carneiro, 25-Aug-2014.) |
|
| ||
| Theorem | elcncf1di 15293* |
Membership in the set of continuous complex functions from to
. (Contributed
by Paul Chapman, 26-Nov-2007.)
|
|
| ||
| Theorem | elcncf1ii 15294* |
Membership in the set of continuous complex functions from to
. (Contributed
by Paul Chapman, 26-Nov-2007.)
|
|
| ||
| Theorem | rescncf 15295 | A continuous complex function restricted to a subset is continuous. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 25-Aug-2014.) |
|
| ||
| Theorem | cncfcdm 15296 | Change the codomain of a continuous complex function. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 1-May-2015.) |
| | ||
| Theorem | cncfss 15297 | The set of continuous functions is expanded when the codomain is expanded. (Contributed by Mario Carneiro, 30-Aug-2014.) |
| | ||
| Theorem | climcncf 15298 | Image of a limit under a continuous map. (Contributed by Mario Carneiro, 7-Apr-2015.) |
 
  | ||
| Theorem | abscncf 15299 | Absolute value is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
|
| ||
| Theorem | recncf 15300 | Real part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
 | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |