HomeTheorem List (p. 252 of 513)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 252 of 513) | < Previous Next > |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-31550) |
Hilbert Space Explorer
(31551-33073) |
Users' Mathboxes
(33074-51270) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | isnmhm2 25101 | A normed module homomorphism is a left module homomorphism with bounded norm (a bounded linear operator). (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑇) ⇒ ⊢ ((𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ∧ 𝐹 ∈ (𝑆 LMHom 𝑇)) → (𝐹 ∈ (𝑆 NMHom 𝑇) ↔ (𝑁‘𝐹) ∈ ℝ)) | ||
| Theorem | nmhmcl 25102 | A normed module homomorphism has a real operator norm. (Contributed by Mario Carneiro, 18-Oct-2015.) |
| ⊢ 𝑁 = (𝑆 normOp 𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 NMHom 𝑇) → (𝑁‘𝐹) ∈ ℝ) | ||
| Theorem | idnmhm 25103 | The identity operator is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.) |
| ⊢ 𝑉 = (Base‘𝑆) ⇒ ⊢ (𝑆 ∈ NrmMod → ( I ↾ 𝑉) ∈ (𝑆 NMHom 𝑆)) | ||
| Theorem | 0nmhm 25104 | The zero operator is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.) |
| ⊢ 𝑉 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑇) & ⊢ 𝐹 = (Scalar‘𝑆) & ⊢ 𝐺 = (Scalar‘𝑇) ⇒ ⊢ ((𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ∧ 𝐹 = 𝐺) → (𝑉 × { 0 }) ∈ (𝑆 NMHom 𝑇)) | ||
| Theorem | nmhmco 25105 | The composition of bounded linear operators is a bounded linear operator. (Contributed by Mario Carneiro, 20-Oct-2015.) |
| ⊢ ((𝐹 ∈ (𝑇 NMHom 𝑈) ∧ 𝐺 ∈ (𝑆 NMHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 NMHom 𝑈)) | ||
| Theorem | nmhmplusg 25106 | The sum of two bounded linear operators is bounded linear. (Contributed by Mario Carneiro, 20-Oct-2015.) |
| ⊢ + = (+g‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 NMHom 𝑇) ∧ 𝐺 ∈ (𝑆 NMHom 𝑇)) → (𝐹 ∘f + 𝐺) ∈ (𝑆 NMHom 𝑇)) | ||
| Theorem | qtopbaslem 25107 | The set of open intervals with endpoints in a subset forms a basis for a topology. (Contributed by Mario Carneiro, 17-Jun-2014.) |
| ⊢ 𝑆 ⊆ ℝ* ⇒ ⊢ ((,) “ (𝑆 × 𝑆)) ∈ TopBases | ||
| Theorem | qtopbas 25108 | The set of open intervals with rational endpoints forms a basis for a topology. (Contributed by NM, 8-Mar-2007.) |
| ⊢ ((,) “ (ℚ × ℚ)) ∈ TopBases | ||
| Theorem | retopbas 25109 | A basis for the standard topology on the reals. (Contributed by NM, 6-Feb-2007.) (Proof shortened by Mario Carneiro, 17-Jun-2014.) |
| ⊢ ran (,) ∈ TopBases | ||
| Theorem | retop 25110 | The standard topology on the reals. (Contributed by FL, 4-Jun-2007.) |
| ⊢ (topGen‘ran (,)) ∈ Top | ||
| Theorem | uniretop 25111 | The underlying set of the standard topology on the reals is the reals. (Contributed by FL, 4-Jun-2007.) |
| ⊢ ℝ = ∪ (topGen‘ran (,)) | ||
| Theorem | retopon 25112 | The standard topology on the reals is a topology on the reals. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ⊢ (topGen‘ran (,)) ∈ (TopOn‘ℝ) | ||
| Theorem | retps 25113 | The standard topological space on the reals. (Contributed by NM, 19-Oct-2012.) |
| ⊢ 𝐾 = {⟨(Base‘ndx), ℝ⟩, ⟨(TopSet‘ndx), (topGen‘ran (,))⟩} ⇒ ⊢ 𝐾 ∈ TopSp | ||
| Theorem | iooretop 25114 | Open intervals are open sets of the standard topology on the reals . (Contributed by FL, 18-Jun-2007.) |
| ⊢ (𝐴(,)𝐵) ∈ (topGen‘ran (,)) | ||
| Theorem | icccld 25115 | Closed intervals are closed sets of the standard topology on ℝ. (Contributed by FL, 14-Sep-2007.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ (Clsd‘(topGen‘ran (,)))) | ||
| Theorem | icopnfcld 25116 | Right-unbounded closed intervals are closed sets of the standard topology on ℝ. (Contributed by Mario Carneiro, 17-Feb-2015.) |
| ⊢ (𝐴 ∈ ℝ → (𝐴[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))) | ||
| Theorem | iocmnfcld 25117 | Left-unbounded closed intervals are closed sets of the standard topology on ℝ. (Contributed by Mario Carneiro, 17-Feb-2015.) |
| ⊢ (𝐴 ∈ ℝ → (-∞(,]𝐴) ∈ (Clsd‘(topGen‘ran (,)))) | ||
| Theorem | qdensere 25118 | ℚ is dense in the standard topology on ℝ. (Contributed by NM, 1-Mar-2007.) |
| ⊢ ((cls‘(topGen‘ran (,)))‘ℚ) = ℝ | ||
| Theorem | cnmetdval 25119 | 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.) |
| ⊢ 𝐷 = (abs ∘ − ) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴𝐷𝐵) = (abs‘(𝐴 − 𝐵))) | ||
| Theorem | cnmet 25120 | 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.) |
| ⊢ (abs ∘ − ) ∈ (Met‘ℂ) | ||
| Theorem | cnxmet 25121 | The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ) | ||
| Theorem | cnbl0 25122 | Two ways to write the open ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.) |
| ⊢ 𝐷 = (abs ∘ − ) ⇒ ⊢ (𝑅 ∈ ℝ* → (◡abs “ (0[,)𝑅)) = (0(ball‘𝐷)𝑅)) | ||
| Theorem | cnblcld 25123* | Two ways to write the closed ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.) |
| ⊢ 𝐷 = (abs ∘ − ) ⇒ ⊢ (𝑅 ∈ ℝ* → (◡abs “ (0[,]𝑅)) = {𝑥 ∈ ℂ ∣ (0𝐷𝑥) ≤ 𝑅}) | ||
| Theorem | cnfldms 25124 | The complex number field is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ⊢ ℂfld ∈ MetSp | ||
| Theorem | cnfldxms 25125 | The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ⊢ ℂfld ∈ ∞MetSp | ||
| Theorem | cnfldtps 25126 | The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ⊢ ℂfld ∈ TopSp | ||
| Theorem | cnfldnm 25127 | The norm of the field of complex numbers. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ abs = (norm‘ℂfld) | ||
| Theorem | cnngp 25128 | The complex numbers form a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ ℂfld ∈ NrmGrp | ||
| Theorem | cnnrg 25129 | The complex numbers form a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ ℂfld ∈ NrmRing | ||
| Theorem | cnfldtopn 25130 | The topology of the complex numbers. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐽 = (MetOpen‘(abs ∘ − )) | ||
| Theorem | cnfldtopon 25131 | The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐽 ∈ (TopOn‘ℂ) | ||
| Theorem | cnfldtop 25132 | The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐽 ∈ Top | ||
| Theorem | cnfldhaus 25133 | The topology of the complex numbers is Hausdorff. (Contributed by Mario Carneiro, 8-Sep-2015.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐽 ∈ Haus | ||
| Theorem | unicntop 25134 | The underlying set of the standard topology on the complex numbers is the set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ ℂ = ∪ (TopOpen‘ℂfld) | ||
| Theorem | cnopn 25135 | The set of complex numbers is open with respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
| ⊢ ℂ ∈ (TopOpen‘ℂfld) | ||
| Theorem | cnn0opn 25136 | The set of nonzero complex numbers is open with respect to the standard topology on complex numbers. (Contributed by SN, 7-Oct-2025.) |
| ⊢ (ℂ ∖ {0}) ∈ (TopOpen‘ℂfld) | ||
| Theorem | zringnrg 25137 | The ring of integers is a normed ring. (Contributed by AV, 13-Jun-2019.) |
| ⊢ ℤring ∈ NrmRing | ||
| Theorem | remetdval 25138 | Value of the distance function of the metric space of real numbers. (Contributed by NM, 16-May-2007.) |
| ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐷𝐵) = (abs‘(𝐴 − 𝐵))) | ||
| Theorem | remet 25139 | The absolute value metric determines a metric space on the reals. (Contributed by NM, 10-Feb-2007.) |
| ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ 𝐷 ∈ (Met‘ℝ) | ||
| Theorem | rexmet 25140 | The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ 𝐷 ∈ (∞Met‘ℝ) | ||
| Theorem | bl2ioo 25141 | A ball in terms of an open interval of reals. (Contributed by NM, 18-May-2007.) (Revised by Mario Carneiro, 13-Nov-2013.) |
| ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴(ball‘𝐷)𝐵) = ((𝐴 − 𝐵)(,)(𝐴 + 𝐵))) | ||
| Theorem | ioo2bl 25142 | An open interval of reals in terms of a ball. (Contributed by NM, 18-May-2007.) (Revised by Mario Carneiro, 28-Aug-2015.) |
| ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴(,)𝐵) = (((𝐴 + 𝐵) / 2)(ball‘𝐷)((𝐵 − 𝐴) / 2))) | ||
| Theorem | ioo2blex 25143 | An open interval of reals in terms of a ball. (Contributed by Mario Carneiro, 14-Nov-2013.) |
| ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴(,)𝐵) ∈ ran (ball‘𝐷)) | ||
| Theorem | blssioo 25144 | 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.) |
| ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ ran (ball‘𝐷) ⊆ ran (,) | ||
| Theorem | tgioo 25145 | 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.) |
| ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (topGen‘ran (,)) = 𝐽 | ||
| Theorem | qdensere2 25146 | ℚ is dense in ℝ. (Contributed by NM, 24-Aug-2007.) |
| ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((cls‘𝐽)‘ℚ) = ℝ | ||
| Theorem | blcvx 25147 | 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.) |
| ⊢ 𝑆 = (𝑃(ball‘(abs ∘ − ))𝑅) ⇒ ⊢ (((𝑃 ∈ ℂ ∧ 𝑅 ∈ ℝ*) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝑇 ∈ (0[,]1))) → ((𝑇 · 𝐴) + ((1 − 𝑇) · 𝐵)) ∈ 𝑆) | ||
| Theorem | rehaus 25148 | The standard topology on the reals is Hausdorff. (Contributed by NM, 8-Mar-2007.) |
| ⊢ (topGen‘ran (,)) ∈ Haus | ||
| Theorem | tgqioo 25149 | 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.) |
| ⊢ 𝑄 = (topGen‘((,) “ (ℚ × ℚ))) ⇒ ⊢ (topGen‘ran (,)) = 𝑄 | ||
| Theorem | re2ndc 25150 | The standard topology on the reals is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
| ⊢ (topGen‘ran (,)) ∈ 2ndω | ||
| Theorem | resubmet 25151 | The subspace topology induced by a subset of the reals. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Aug-2014.) |
| ⊢ 𝑅 = (topGen‘ran (,)) & ⊢ 𝐽 = (MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴))) ⇒ ⊢ (𝐴 ⊆ ℝ → 𝐽 = (𝑅 ↾t 𝐴)) | ||
| Theorem | tgioo2 25152 | The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (topGen‘ran (,)) = (𝐽 ↾t ℝ) | ||
| Theorem | rerest 25153 | The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 13-Aug-2014.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝑅 = (topGen‘ran (,)) ⇒ ⊢ (𝐴 ⊆ ℝ → (𝐽 ↾t 𝐴) = (𝑅 ↾t 𝐴)) | ||
| Theorem | tgioo4 25154 | The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Glauco Siliprandi, 5-Feb-2022.) |
| ⊢ (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ) | ||
| Theorem | tgioo3 25155 | 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.) |
| ⊢ 𝐽 = (TopOpen‘ℝfld) ⇒ ⊢ (topGen‘ran (,)) = 𝐽 | ||
| Theorem | xrtgioo 25156 | 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 ℝ) ⇒ ⊢ (topGen‘ran (,)) = 𝐽 | ||
| Theorem | xrrest 25157 | The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 9-Sep-2015.) |
| ⊢ 𝑋 = (ordTop‘ ≤ ) & ⊢ 𝑅 = (topGen‘ran (,)) ⇒ ⊢ (𝐴 ⊆ ℝ → (𝑋 ↾t 𝐴) = (𝑅 ↾t 𝐴)) | ||
| Theorem | xrrest2 25158 | The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 9-Sep-2015.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝑋 = (ordTop‘ ≤ ) ⇒ ⊢ (𝐴 ⊆ ℝ → (𝐽 ↾t 𝐴) = (𝑋 ↾t 𝐴)) | ||
| Theorem | xrsxmet 25159 | The metric on the extended reals is a proper extended metric. (Contributed by Mario Carneiro, 4-Sep-2015.) |
| ⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ 𝐷 ∈ (∞Met‘ℝ*) | ||
| Theorem | xrsdsre 25160 | The metric on the extended reals coincides with the usual metric on the reals. (Contributed by Mario Carneiro, 4-Sep-2015.) |
| ⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ (𝐷 ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ)) | ||
| Theorem | xrsblre 25161 | 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.) |
| ⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ ((𝑃 ∈ ℝ ∧ 𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) ⊆ ℝ) | ||
| Theorem | xrsmopn 25162 | 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.) |
| ⊢ 𝐷 = (dist‘ℝ*𝑠) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (ordTop‘ ≤ ) ⊆ 𝐽 | ||
| Theorem | zcld 25163 | The integers are a closed set in the topology on ℝ. (Contributed by Mario Carneiro, 17-Feb-2015.) |
| ⊢ 𝐽 = (topGen‘ran (,)) ⇒ ⊢ ℤ ∈ (Clsd‘𝐽) | ||
| Theorem | recld2 25164 | The real numbers are a closed set in the topology on ℂ. (Contributed by Mario Carneiro, 17-Feb-2015.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ ℝ ∈ (Clsd‘𝐽) | ||
| Theorem | zcld2 25165 | The integers are a closed set in the topology on ℂ. (Contributed by Mario Carneiro, 17-Feb-2015.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ ℤ ∈ (Clsd‘𝐽) | ||
| Theorem | zdis 25166 | The integers are a discrete set in the topology on ℂ. (Contributed by Mario Carneiro, 19-Sep-2015.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝐽 ↾t ℤ) = 𝒫 ℤ | ||
| Theorem | sszcld 25167 | Every subset of the integers are closed in the topology on ℂ. (Contributed by Mario Carneiro, 6-Jul-2017.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝐴 ⊆ ℤ → 𝐴 ∈ (Clsd‘𝐽)) | ||
| Theorem | reperflem 25168* | A subset of the real numbers that is closed under addition with real numbers is perfect. (Contributed by Mario Carneiro, 26-Dec-2016.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ ((𝑢 ∈ 𝑆 ∧ 𝑣 ∈ ℝ) → (𝑢 + 𝑣) ∈ 𝑆) & ⊢ 𝑆 ⊆ ℂ ⇒ ⊢ (𝐽 ↾t 𝑆) ∈ Perf | ||
| Theorem | reperf 25169 | The real numbers are a perfect subset of the complex numbers. (Contributed by Mario Carneiro, 26-Dec-2016.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝐽 ↾t ℝ) ∈ Perf | ||
| Theorem | cnperf 25170 | The complex numbers are a perfect space. (Contributed by Mario Carneiro, 26-Dec-2016.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐽 ∈ Perf | ||
| Theorem | iccntr 25171 | The interior of a closed interval in the standard topology on ℝ is the corresponding open interval. (Contributed by Mario Carneiro, 1-Sep-2014.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((int‘(topGen‘ran (,)))‘(𝐴[,]𝐵)) = (𝐴(,)𝐵)) | ||
| Theorem | icccmplem1 25172* | Lemma for icccmp 25175. (Contributed by Mario Carneiro, 18-Jun-2014.) |
| ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵)) & ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) & ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝑈 ⊆ 𝐽) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) ⇒ ⊢ (𝜑 → (𝐴 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵)) | ||
| Theorem | icccmplem2 25173* | Lemma for icccmp 25175. (Contributed by Mario Carneiro, 13-Jun-2014.) |
| ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵)) & ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) & ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝑈 ⊆ 𝐽) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) & ⊢ (𝜑 → 𝑉 ∈ 𝑈) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → (𝐺(ball‘𝐷)𝐶) ⊆ 𝑉) & ⊢ 𝐺 = sup(𝑆, ℝ, < ) & ⊢ 𝑅 = if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑆) | ||
| Theorem | icccmplem3 25174* | Lemma for icccmp 25175. (Contributed by Mario Carneiro, 13-Jun-2014.) |
| ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵)) & ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) & ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝑈 ⊆ 𝐽) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑆) | ||
| Theorem | icccmp 25175 | A closed interval in ℝ is compact. (Contributed by Mario Carneiro, 13-Jun-2014.) |
| ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑇 ∈ Comp) | ||
| Theorem | reconnlem1 25176 | Lemma for reconn 25178. Connectedness in the reals-easy direction. (Contributed by Jeff Hankins, 13-Jul-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.) |
| ⊢ (((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Conn) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → (𝑋[,]𝑌) ⊆ 𝐴) | ||
| Theorem | reconnlem2 25177* | Lemma for reconn 25178. (Contributed by Jeff Hankins, 17-Aug-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝑈 ∈ (topGen‘ran (,))) & ⊢ (𝜑 → 𝑉 ∈ (topGen‘ran (,))) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ (𝑈 ∩ 𝐴)) & ⊢ (𝜑 → 𝐶 ∈ (𝑉 ∩ 𝐴)) & ⊢ (𝜑 → (𝑈 ∩ 𝑉) ⊆ (ℝ ∖ 𝐴)) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) & ⊢ 𝑆 = sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ⇒ ⊢ (𝜑 → ¬ 𝐴 ⊆ (𝑈 ∪ 𝑉)) | ||
| Theorem | reconn 25178* | 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.) |
| ⊢ (𝐴 ⊆ ℝ → (((topGen‘ran (,)) ↾t 𝐴) ∈ Conn ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴)) | ||
| Theorem | retopconn 25179 | Corollary of reconn 25178. The set of real numbers is connected. (Contributed by Jeff Hankins, 17-Aug-2009.) |
| ⊢ (topGen‘ran (,)) ∈ Conn | ||
| Theorem | iccconn 25180 | A closed interval is connected. (Contributed by Jeff Hankins, 17-Aug-2009.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ Conn) | ||
| Theorem | opnreen 25181 | Every nonempty open set is uncountable. (Contributed by Mario Carneiro, 26-Jul-2014.) (Revised by Mario Carneiro, 20-Feb-2015.) |
| ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → 𝐴 ≈ 𝒫 ℕ) | ||
| Theorem | rectbntr0 25182 | A countable subset of the reals has empty interior. (Contributed by Mario Carneiro, 26-Jul-2014.) |
| ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ) → ((int‘(topGen‘ran (,)))‘𝐴) = ∅) | ||
| Theorem | xrge0gsumle 25183 | A finite sum in the nonnegative extended reals is monotonic in the support. (Contributed by Mario Carneiro, 13-Sep-2015.) |
| ⊢ 𝐺 = (ℝ*𝑠 ↾s (0[,]+∞)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐵 ∈ (𝒫 𝐴 ∩ Fin)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ 𝐶)) ≤ (𝐺 Σg (𝐹 ↾ 𝐵))) | ||
| Theorem | xrge0tsms 25184* | 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 (0[,]+∞)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶(0[,]+∞)) & ⊢ 𝑆 = sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, < ) ⇒ ⊢ (𝜑 → (𝐺 tsums 𝐹) = {𝑆}) | ||
| Theorem | xrge0tsms2 25185 | Any finite or infinite sum in the nonnegative extended reals is convergent. This is a rather unique property of the set [0, +∞]; a similar theorem is not true for ℝ* or ℝ or [0, +∞). It is true for ℕ0 ∪ {+∞}, however, or more generally any additive submonoid of [0, +∞) with +∞ adjoined. (Contributed by Mario Carneiro, 13-Sep-2015.) |
| ⊢ 𝐺 = (ℝ*𝑠 ↾s (0[,]+∞)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶(0[,]+∞)) → (𝐺 tsums 𝐹) ≈ 1o) | ||
| Theorem | metdcnlem 25186 | 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.) |
| ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐶 = (dist‘ℝ*𝑠) & ⊢ 𝐾 = (MetOpen‘𝐶) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ (𝜑 → 𝑍 ∈ 𝑋) & ⊢ (𝜑 → (𝐴𝐷𝑌) < (𝑅 / 2)) & ⊢ (𝜑 → (𝐵𝐷𝑍) < (𝑅 / 2)) ⇒ ⊢ (𝜑 → ((𝐴𝐷𝐵)𝐶(𝑌𝐷𝑍)) < 𝑅) | ||
| Theorem | xmetdcn2 25187 | The metric function of an extended metric space is always continuous in the topology generated by it. In this variation of xmetdcn 25188 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.) |
| ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐶 = (dist‘ℝ*𝑠) & ⊢ 𝐾 = (MetOpen‘𝐶) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷 ∈ ((𝐽 ×t 𝐽) Cn 𝐾)) | ||
| Theorem | xmetdcn 25188 | The metric function of an extended metric space is always continuous in the topology generated by it. (Contributed by Mario Carneiro, 4-Sep-2015.) |
| ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = (ordTop‘ ≤ ) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷 ∈ ((𝐽 ×t 𝐽) Cn 𝐾)) | ||
| Theorem | metdcn2 25189 | 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.) |
| ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = (topGen‘ran (,)) ⇒ ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ ((𝐽 ×t 𝐽) Cn 𝐾)) | ||
| Theorem | metdcn 25190 | 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.) |
| ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ ((𝐽 ×t 𝐽) Cn 𝐾)) | ||
| Theorem | msdcn 25191 | 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.) |
| ⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = (dist‘𝑀) & ⊢ 𝐽 = (TopOpen‘𝑀) & ⊢ 𝐾 = (topGen‘ran (,)) ⇒ ⊢ (𝑀 ∈ MetSp → (𝐷 ↾ (𝑋 × 𝑋)) ∈ ((𝐽 ×t 𝐽) Cn 𝐾)) | ||
| Theorem | cnmpt1ds 25192* | Continuity of the metric function; analogue of cnmpt12f 24015 which cannot be used directly because 𝐷 is not necessarily a function. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| ⊢ 𝐷 = (dist‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ 𝑅 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐺 ∈ MetSp) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐾 Cn 𝐽)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐾 Cn 𝐽)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴𝐷𝐵)) ∈ (𝐾 Cn 𝑅)) | ||
| Theorem | cnmpt2ds 25193* | Continuity of the metric function; analogue of cnmpt22f 24024 which cannot be used directly because 𝐷 is not necessarily a function. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| ⊢ 𝐷 = (dist‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ 𝑅 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐺 ∈ MetSp) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐾 ×t 𝐿) Cn 𝐽)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐾 ×t 𝐿) Cn 𝐽)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐴𝐷𝐵)) ∈ ((𝐾 ×t 𝐿) Cn 𝑅)) | ||
| Theorem | nmcn 25194 | The norm of a normed group is a continuous function. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ 𝑁 = (norm‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ 𝐾 = (topGen‘ran (,)) ⇒ ⊢ (𝐺 ∈ NrmGrp → 𝑁 ∈ (𝐽 Cn 𝐾)) | ||
| Theorem | ngnmcncn 25195 | The norm of a normed group is a continuous function to ℂ. (Contributed by NM, 12-Aug-2007.) (Revised by AV, 17-Oct-2021.) |
| ⊢ 𝑁 = (norm‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) & ⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ (𝐺 ∈ NrmGrp → 𝑁 ∈ (𝐽 Cn 𝐾)) | ||
| Theorem | abscn 25196 | The absolute value function on complex numbers is continuous. (Contributed by NM, 22-Aug-2007.) (Proof shortened by Mario Carneiro, 10-Jan-2014.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (topGen‘ran (,)) ⇒ ⊢ abs ∈ (𝐽 Cn 𝐾) | ||
| Theorem | metdsval 25197* | 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(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < )) ⇒ ⊢ (𝐴 ∈ 𝑋 → (𝐹‘𝐴) = inf(ran (𝑦 ∈ 𝑆 ↦ (𝐴𝐷𝑦)), ℝ*, < )) | ||
| Theorem | metdsf 25198* | 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(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < )) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝐹:𝑋⟶(0[,]+∞)) | ||
| Theorem | metdsge 25199* | 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(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < )) ⇒ ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ 𝑅 ∈ ℝ*) → (𝑅 ≤ (𝐹‘𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)𝑅)) = ∅)) | ||
| Theorem | metds0 25200* | 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(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < )) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆) → (𝐹‘𝐴) = 0) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |