HomeTheorem List (p. 141 of 149)
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. 141 of 149) | < 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 | metss2 14001* |
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.)
|
           
 ![/\](wedge.gif "/\"){kind=small}
  | ||
| Theorem | comet 14002* | 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 14003* | Value of the standard bounded metric. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 9-May-2023.) |
 inf    
inf
| ||
| Theorem | bdxmet 14004* | 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 14005* | 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 14006* |
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 14007* |
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 14008* | 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 14009 | 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 14010* | The maximum metric (Chebyshev distance) on the product of two sets. (Contributed by Jim Kingdon, 11-Oct-2023.) |
      
| ||
| Theorem | xmetxpbl 14011* |
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 14012* | Lemma for xmettx 14013. (Contributed by Jim Kingdon, 15-Oct-2023.) |
  | ||
| Theorem | xmettx 14013* | 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 14014* |
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 14015* |
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 14016* |
Two ways to say a mapping from metric to metric is
continuous at point . The distance arguments are swapped compared
to metcnp 14015 (and Munkres' metcn 14017) for compatibility with df-lm 13693.
Definition 1.3-3 of [Kreyszig] p. 20.
(Contributed by NM, 4-Jun-2007.)
(Revised by Mario Carneiro, 13-Nov-2013.)
|
| | ||
| Theorem | metcn 14017* |
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 14018* | Epsilon-delta property of a continuous metric space function, with function arguments as in metcnp 14015. (Contributed by NM, 17-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
|
| ||
| Theorem | metcnpi2 14019* | Epsilon-delta property of a continuous metric space function, with swapped distance function arguments as in metcnp2 14016. (Contributed by NM, 16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
|
| ||
| Theorem | metcnpi3 14020* |
Epsilon-delta property of a metric space function continuous at .
A variation of metcnpi2 14019 with non-strict ordering. (Contributed by
NM,
16-Dec-2007.) (Revised by Mario Carneiro, 13-Nov-2013.)
|
|
| ||
| Theorem | txmetcnp 14021* | Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.) (Revised by Jim Kingdon, 22-Oct-2023.) |
 
 
| ||
| Theorem | txmetcn 14022* | Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.) |
|
| ||
| Theorem | metcnpd 14023* |
Two ways to say a mapping from metric to metric is
continuous at point . (Contributed by Jim Kingdon,
14-Jun-2023.)
|
|
| ||
| Theorem | qtopbasss 14024* | 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 14025 | The set of open intervals with rational endpoints forms a basis for a topology. (Contributed by NM, 8-Mar-2007.) |
 | ||
| Theorem | retopbas 14026 | 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 14027 | The standard topology on the reals. (Contributed by FL, 4-Jun-2007.) |
  | ||
| Theorem | uniretop 14028 | The underlying set of the standard topology on the reals is the reals. (Contributed by FL, 4-Jun-2007.) |
 
| ||
| Theorem | retopon 14029 | The standard topology on the reals is a topology on the reals. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| TopOn | ||
| Theorem | retps 14030 | The standard topological space on the reals. (Contributed by NM, 19-Oct-2012.) |
  TopSet
 | ||
| Theorem | iooretopg 14031 | 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 14032 | 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 14033 | 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 14034 | The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
|
| ||
| Theorem | cntoptopon 14035 | The topology of the complex numbers is a topology. (Contributed by Jim Kingdon, 6-Jun-2023.) |
| TopOn | ||
| Theorem | cntoptop 14036 | The topology of the complex numbers is a topology. (Contributed by Jim Kingdon, 6-Jun-2023.) |
| | ||
| Theorem | cnbl0 14037 | Two ways to write the open ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.) |
  | ||
| Theorem | cnblcld 14038* | Two ways to write the closed ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.) |
 | ||
| Theorem | unicntopcntop 14039 | 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 | cnopncntop 14040 | 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 | reopnap 14041* | The real numbers apart from a given real number form an open set. (Contributed by Jim Kingdon, 13-Dec-2023.) |
| #
| ||
| Theorem | remetdval 14042 | Value of the distance function of the metric space of real numbers. (Contributed by NM, 16-May-2007.) |
|
| ||
| Theorem | remet 14043 | The absolute value metric determines a metric space on the reals. (Contributed by NM, 10-Feb-2007.) |
| | ||
| Theorem | rexmet 14044 | The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| | ||
| Theorem | bl2ioo 14045 | 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 14046 | 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 14047 | An open interval of reals in terms of a ball. (Contributed by Mario Carneiro, 14-Nov-2013.) |
| | ||
| Theorem | blssioo 14048 | 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 14049 | 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 14050 | 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 14051 | 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 14052 | 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 14053 | 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 | addcncntoplem 14054* | Lemma for addcncntop 14055, subcncntop 14056, and mulcncntop 14057. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Jim Kingdon, 22-Oct-2023.) |
   
| ||
| Theorem | addcncntop 14055 | 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 14056 | 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 14057 | 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 14058* | 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 | fsumcncntop 14059* |
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 
| ||
| Syntax | ccncf 14060 | Extend class notation to include the operation which returns a class of continuous complex functions. |
  | ||
| Definition | df-cncf 14061* | Define the operation whose value is a class of continuous complex functions. (Contributed by Paul Chapman, 11-Oct-2007.) |
  
 | ||
| Theorem | cncfval 14062* |
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 14063* |
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 14064* | Version of elcncf 14063 with arguments commuted. (Contributed by Mario Carneiro, 28-Apr-2014.) |
| | ||
| Theorem | cncfrss 14065 | Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.) |
| | ||
| Theorem | cncfrss2 14066 | Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.) |
| | ||
| Theorem | cncff 14067 | A continuous complex function's domain and codomain. (Contributed by Paul Chapman, 17-Jan-2008.) (Revised by Mario Carneiro, 25-Aug-2014.) |
| | ||
| Theorem | cncfi 14068* | Defining property of a continuous function. (Contributed by Mario Carneiro, 30-Apr-2014.) (Revised by Mario Carneiro, 25-Aug-2014.) |
|
| ||
| Theorem | elcncf1di 14069* |
Membership in the set of continuous complex functions from to
. (Contributed
by Paul Chapman, 26-Nov-2007.)
|
|
| ||
| Theorem | elcncf1ii 14070* |
Membership in the set of continuous complex functions from to
. (Contributed
by Paul Chapman, 26-Nov-2007.)
|
|
| ||
| Theorem | rescncf 14071 | 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 14072 | Change the codomain of a continuous complex function. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 1-May-2015.) |
| | ||
| Theorem | cncfss 14073 | The set of continuous functions is expanded when the codomain is expanded. (Contributed by Mario Carneiro, 30-Aug-2014.) |
| | ||
| Theorem | climcncf 14074 | Image of a limit under a continuous map. (Contributed by Mario Carneiro, 7-Apr-2015.) |
 
  | ||
| Theorem | abscncf 14075 | Absolute value is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
|
| ||
| Theorem | recncf 14076 | Real part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
 | ||
| Theorem | imcncf 14077 | Imaginary part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
 | ||
| Theorem | cjcncf 14078 | Complex conjugate is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
 | ||
| Theorem | mulc1cncf 14079* | Multiplication by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
|
| ||
| Theorem | divccncfap 14080* | Division by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Jim Kingdon, 9-Jan-2023.) |
| # | ||
| Theorem | cncfco 14081 | The composition of two continuous maps on complex numbers is also continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 25-Aug-2014.) |
| | ||
| Theorem | cncfmet 14082 | Relate complex function continuity to metric space continuity. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.) |
|
| ||
| Theorem | cncfcncntop 14083 | Relate complex function continuity to topological continuity. (Contributed by Mario Carneiro, 17-Feb-2015.) |
| ↾t ↾t
| ||
| Theorem | cncfcn1cntop 14084 | Relate complex function continuity to topological continuity. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.) (Revised by Jim Kingdon, 16-Jun-2023.) |
| | ||
| Theorem | cncfmptc 14085* |
A constant function is a continuous function on . (Contributed
by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro,
7-Sep-2015.)
|
| ||
| Theorem | cncfmptid 14086* |
The identity function is a continuous function on . (Contributed
by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro,
17-May-2016.)
|
| | ||
| Theorem | cncfmpt1f 14087* |
Composition of continuous functions. analogue of cnmpt11f 13787.
(Contributed by Mario Carneiro, 3-Sep-2014.)
|
|
| ||
| Theorem | cncfmpt2fcntop 14088* |
Composition of continuous functions. analogue of cnmpt12f 13789.
(Contributed by Mario Carneiro, 3-Sep-2014.)
|
|
| ||
| Theorem | addccncf 14089* | Adding a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) |
|
| ||
| Theorem | cdivcncfap 14090* | Division with a constant numerator is continuous. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 26-May-2023.) |
| #
#
| ||
| Theorem | negcncf 14091* | The negative function is continuous. (Contributed by Mario Carneiro, 30-Dec-2016.) |
 | ||
| Theorem | negfcncf 14092* | The negative of a continuous complex function is continuous. (Contributed by Paul Chapman, 21-Jan-2008.) (Revised by Mario Carneiro, 25-Aug-2014.) |
|
| ||
| Theorem | mulcncflem 14093* | Lemma for mulcncf 14094. (Contributed by Jim Kingdon, 29-May-2023.) |
 
![]_](_urbrack.gif "]_"){kind=small}
| ||
| Theorem | mulcncf 14094* | The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
|
| ||
| Theorem | expcncf 14095* | The power function on complex numbers, for fixed exponent N, is continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
 | ||
| Theorem | cnrehmeocntop 14096* |
The canonical bijection from to described in
cnref1o 9650 is in fact a homeomorphism of the usual
topologies on these
sets. (It is also an isometry, if
is metrized with the
l<SUP>2</SUP> norm.) (Contributed by Mario Carneiro,
25-Aug-2014.)
|
 | ||
| Theorem | cnopnap 14097* | The complex numbers apart from a given complex number form an open set. (Contributed by Jim Kingdon, 14-Dec-2023.) |
| #
| ||
| Theorem | dedekindeulemuub 14098* | Lemma for dedekindeu 14104. Any element of the upper cut is an upper bound for the lower cut. (Contributed by Jim Kingdon, 2-Feb-2024.) |
  
 
| ||
| Theorem | dedekindeulemub 14099* | Lemma for dedekindeu 14104. The lower cut has an upper bound. (Contributed by Jim Kingdon, 31-Jan-2024.) |
|
| ||
| Theorem | dedekindeulemloc 14100* | Lemma for dedekindeu 14104. The set L is located. (Contributed by Jim Kingdon, 31-Jan-2024.) |
|
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |