HomeTheorem List (p. 249 of 491)
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. 249 of 491) | < 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-30946) |
Hilbert Space Explorer
(30947-32469) |
Users' Mathboxes
(32470-49035) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | iooretop 24801 | Open intervals are open sets of the standard topology on the reals . (Contributed by FL, 18-Jun-2007.) |
| ⊢ (𝐴(,)𝐵) ∈ (topGen‘ran (,)) | ||
| Theorem | icccld 24802 | Closed intervals are closed sets of the standard topology on ℝ. (Contributed by FL, 14-Sep-2007.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ (Clsd‘(topGen‘ran (,)))) | ||
| Theorem | icopnfcld 24803 | Right-unbounded closed intervals are closed sets of the standard topology on ℝ. (Contributed by Mario Carneiro, 17-Feb-2015.) |
| ⊢ (𝐴 ∈ ℝ → (𝐴[,)+∞) ∈ (Clsd‘(topGen‘ran (,)))) | ||
| Theorem | iocmnfcld 24804 | Left-unbounded closed intervals are closed sets of the standard topology on ℝ. (Contributed by Mario Carneiro, 17-Feb-2015.) |
| ⊢ (𝐴 ∈ ℝ → (-∞(,]𝐴) ∈ (Clsd‘(topGen‘ran (,)))) | ||
| Theorem | qdensere 24805 | ℚ is dense in the standard topology on ℝ. (Contributed by NM, 1-Mar-2007.) |
| ⊢ ((cls‘(topGen‘ran (,)))‘ℚ) = ℝ | ||
| Theorem | cnmetdval 24806 | 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 24807 | 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 24808 | The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ) | ||
| Theorem | cnbl0 24809 | Two ways to write the open ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.) |
| ⊢ 𝐷 = (abs ∘ − ) ⇒ ⊢ (𝑅 ∈ ℝ* → (◡abs “ (0[,)𝑅)) = (0(ball‘𝐷)𝑅)) | ||
| Theorem | cnblcld 24810* | Two ways to write the closed ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015.) |
| ⊢ 𝐷 = (abs ∘ − ) ⇒ ⊢ (𝑅 ∈ ℝ* → (◡abs “ (0[,]𝑅)) = {𝑥 ∈ ℂ ∣ (0𝐷𝑥) ≤ 𝑅}) | ||
| Theorem | cnfldms 24811 | The complex number field is a metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ⊢ ℂfld ∈ MetSp | ||
| Theorem | cnfldxms 24812 | The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ⊢ ℂfld ∈ ∞MetSp | ||
| Theorem | cnfldtps 24813 | The complex number field is a topological space. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ⊢ ℂfld ∈ TopSp | ||
| Theorem | cnfldnm 24814 | The norm of the field of complex numbers. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ abs = (norm‘ℂfld) | ||
| Theorem | cnngp 24815 | The complex numbers form a normed group. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ ℂfld ∈ NrmGrp | ||
| Theorem | cnnrg 24816 | The complex numbers form a normed ring. (Contributed by Mario Carneiro, 4-Oct-2015.) |
| ⊢ ℂfld ∈ NrmRing | ||
| Theorem | cnfldtopn 24817 | The topology of the complex numbers. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐽 = (MetOpen‘(abs ∘ − )) | ||
| Theorem | cnfldtopon 24818 | The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐽 ∈ (TopOn‘ℂ) | ||
| Theorem | cnfldtop 24819 | The topology of the complex numbers is a topology. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐽 ∈ Top | ||
| Theorem | cnfldhaus 24820 | The topology of the complex numbers is Hausdorff. (Contributed by Mario Carneiro, 8-Sep-2015.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐽 ∈ Haus | ||
| Theorem | unicntop 24821 | 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 24822 | 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 | zringnrg 24823 | The ring of integers is a normed ring. (Contributed by AV, 13-Jun-2019.) |
| ⊢ ℤring ∈ NrmRing | ||
| Theorem | remetdval 24824 | Value of the distance function of the metric space of real numbers. (Contributed by NM, 16-May-2007.) |
| ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐷𝐵) = (abs‘(𝐴 − 𝐵))) | ||
| Theorem | remet 24825 | The absolute value metric determines a metric space on the reals. (Contributed by NM, 10-Feb-2007.) |
| ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ 𝐷 ∈ (Met‘ℝ) | ||
| Theorem | rexmet 24826 | The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
| ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ 𝐷 ∈ (∞Met‘ℝ) | ||
| Theorem | bl2ioo 24827 | 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 24828 | 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 24829 | An open interval of reals in terms of a ball. (Contributed by Mario Carneiro, 14-Nov-2013.) |
| ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴(,)𝐵) ∈ ran (ball‘𝐷)) | ||
| Theorem | blssioo 24830 | 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 24831 | 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 24832 | ℚ is dense in ℝ. (Contributed by NM, 24-Aug-2007.) |
| ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((cls‘𝐽)‘ℚ) = ℝ | ||
| Theorem | blcvx 24833 | 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 24834 | The standard topology on the reals is Hausdorff. (Contributed by NM, 8-Mar-2007.) |
| ⊢ (topGen‘ran (,)) ∈ Haus | ||
| Theorem | tgqioo 24835 | 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 24836 | The standard topology on the reals is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
| ⊢ (topGen‘ran (,)) ∈ 2ndω | ||
| Theorem | resubmet 24837 | 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 24838 | 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 24839 | The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 13-Aug-2014.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝑅 = (topGen‘ran (,)) ⇒ ⊢ (𝐴 ⊆ ℝ → (𝐽 ↾t 𝐴) = (𝑅 ↾t 𝐴)) | ||
| Theorem | tgioo3 24840 | 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 24841 | 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 24842 | The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 9-Sep-2015.) |
| ⊢ 𝑋 = (ordTop‘ ≤ ) & ⊢ 𝑅 = (topGen‘ran (,)) ⇒ ⊢ (𝐴 ⊆ ℝ → (𝑋 ↾t 𝐴) = (𝑅 ↾t 𝐴)) | ||
| Theorem | xrrest2 24843 | The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 9-Sep-2015.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝑋 = (ordTop‘ ≤ ) ⇒ ⊢ (𝐴 ⊆ ℝ → (𝐽 ↾t 𝐴) = (𝑋 ↾t 𝐴)) | ||
| Theorem | xrsxmet 24844 | The metric on the extended reals is a proper extended metric. (Contributed by Mario Carneiro, 4-Sep-2015.) |
| ⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ 𝐷 ∈ (∞Met‘ℝ*) | ||
| Theorem | xrsdsre 24845 | 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 24846 | 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 24847 | 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 24848 | The integers are a closed set in the topology on ℝ. (Contributed by Mario Carneiro, 17-Feb-2015.) |
| ⊢ 𝐽 = (topGen‘ran (,)) ⇒ ⊢ ℤ ∈ (Clsd‘𝐽) | ||
| Theorem | recld2 24849 | The real numbers are a closed set in the topology on ℂ. (Contributed by Mario Carneiro, 17-Feb-2015.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ ℝ ∈ (Clsd‘𝐽) | ||
| Theorem | zcld2 24850 | The integers are a closed set in the topology on ℂ. (Contributed by Mario Carneiro, 17-Feb-2015.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ ℤ ∈ (Clsd‘𝐽) | ||
| Theorem | zdis 24851 | The integers are a discrete set in the topology on ℂ. (Contributed by Mario Carneiro, 19-Sep-2015.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝐽 ↾t ℤ) = 𝒫 ℤ | ||
| Theorem | sszcld 24852 | Every subset of the integers are closed in the topology on ℂ. (Contributed by Mario Carneiro, 6-Jul-2017.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝐴 ⊆ ℤ → 𝐴 ∈ (Clsd‘𝐽)) | ||
| Theorem | reperflem 24853* | 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 24854 | The real numbers are a perfect subset of the complex numbers. (Contributed by Mario Carneiro, 26-Dec-2016.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝐽 ↾t ℝ) ∈ Perf | ||
| Theorem | cnperf 24855 | The complex numbers are a perfect space. (Contributed by Mario Carneiro, 26-Dec-2016.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐽 ∈ Perf | ||
| Theorem | iccntr 24856 | 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 24857* | Lemma for icccmp 24860. (Contributed by Mario Carneiro, 18-Jun-2014.) |
| ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵)) & ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) & ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝑈 ⊆ 𝐽) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) ⇒ ⊢ (𝜑 → (𝐴 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵)) | ||
| Theorem | icccmplem2 24858* | Lemma for icccmp 24860. (Contributed by Mario Carneiro, 13-Jun-2014.) |
| ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵)) & ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) & ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝑈 ⊆ 𝐽) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) & ⊢ (𝜑 → 𝑉 ∈ 𝑈) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → (𝐺(ball‘𝐷)𝐶) ⊆ 𝑉) & ⊢ 𝐺 = sup(𝑆, ℝ, < ) & ⊢ 𝑅 = if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑆) | ||
| Theorem | icccmplem3 24859* | Lemma for icccmp 24860. (Contributed by Mario Carneiro, 13-Jun-2014.) |
| ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵)) & ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) & ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝑈 ⊆ 𝐽) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑆) | ||
| Theorem | icccmp 24860 | A closed interval in ℝ is compact. (Contributed by Mario Carneiro, 13-Jun-2014.) |
| ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑇 ∈ Comp) | ||
| Theorem | reconnlem1 24861 | Lemma for reconn 24863. 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 24862* | Lemma for reconn 24863. (Contributed by Jeff Hankins, 17-Aug-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.) |
| ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝑈 ∈ (topGen‘ran (,))) & ⊢ (𝜑 → 𝑉 ∈ (topGen‘ran (,))) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ (𝑈 ∩ 𝐴)) & ⊢ (𝜑 → 𝐶 ∈ (𝑉 ∩ 𝐴)) & ⊢ (𝜑 → (𝑈 ∩ 𝑉) ⊆ (ℝ ∖ 𝐴)) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) & ⊢ 𝑆 = sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ⇒ ⊢ (𝜑 → ¬ 𝐴 ⊆ (𝑈 ∪ 𝑉)) | ||
| Theorem | reconn 24863* | 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 24864 | Corollary of reconn 24863. The set of real numbers is connected. (Contributed by Jeff Hankins, 17-Aug-2009.) |
| ⊢ (topGen‘ran (,)) ∈ Conn | ||
| Theorem | iccconn 24865 | A closed interval is connected. (Contributed by Jeff Hankins, 17-Aug-2009.) |
| ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ Conn) | ||
| Theorem | opnreen 24866 | Every nonempty open set is uncountable. (Contributed by Mario Carneiro, 26-Jul-2014.) (Revised by Mario Carneiro, 20-Feb-2015.) |
| ⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → 𝐴 ≈ 𝒫 ℕ) | ||
| Theorem | rectbntr0 24867 | A countable subset of the reals has empty interior. (Contributed by Mario Carneiro, 26-Jul-2014.) |
| ⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ) → ((int‘(topGen‘ran (,)))‘𝐴) = ∅) | ||
| Theorem | xrge0gsumle 24868 | 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 24869* | 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 24870 | 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 24871 | 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 24872 | The metric function of an extended metric space is always continuous in the topology generated by it. In this variation of xmetdcn 24873 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 24873 | 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 24874 | 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 24875 | 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 24876 | 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 24877* | Continuity of the metric function; analogue of cnmpt12f 23689 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 24878* | Continuity of the metric function; analogue of cnmpt22f 23698 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 24879 | 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 24880 | 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 24881 | 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 24882* | 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 24883* | 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 24884* | 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 24885* | 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) | ||
| Theorem | metdstri 24886* | 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(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < )) ⇒ ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐴) ≤ ((𝐴𝐷𝐵) +𝑒 (𝐹‘𝐵))) | ||
| Theorem | metdsle 24887* | 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(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < )) ⇒ ⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋)) → (𝐹‘𝐵) ≤ (𝐴𝐷𝐵)) | ||
| Theorem | metdsre 24888* | 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(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < )) ⇒ ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → 𝐹:𝑋⟶ℝ) | ||
| Theorem | metdseq0 24889* | 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(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < )) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → ((𝐹‘𝐴) = 0 ↔ 𝐴 ∈ ((cls‘𝐽)‘𝑆))) | ||
| Theorem | metdscnlem 24890* | Lemma for metdscn 24891. (Contributed by Mario Carneiro, 4-Sep-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < )) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐶 = (dist‘ℝ*𝑠) & ⊢ 𝐾 = (MetOpen‘𝐶) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → (𝐴𝐷𝐵) < 𝑅) ⇒ ⊢ (𝜑 → ((𝐹‘𝐴) +𝑒 -𝑒(𝐹‘𝐵)) < 𝑅) | ||
| Theorem | metdscn 24891* | 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(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < )) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐶 = (dist‘ℝ*𝑠) & ⊢ 𝐾 = (MetOpen‘𝐶) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → 𝐹 ∈ (𝐽 Cn 𝐾)) | ||
| Theorem | metdscn2 24892* | 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(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < )) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → 𝐹 ∈ (𝐽 Cn 𝐾)) | ||
| Theorem | metnrmlem1a 24893* | Lemma for metnrm 24897. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Mario Carneiro, 4-Sep-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < )) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐽)) & ⊢ (𝜑 → 𝑇 ∈ (Clsd‘𝐽)) & ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑇) → (0 < (𝐹‘𝐴) ∧ if(1 ≤ (𝐹‘𝐴), 1, (𝐹‘𝐴)) ∈ ℝ+)) | ||
| Theorem | metnrmlem1 24894* | Lemma for metnrm 24897. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Mario Carneiro, 4-Sep-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < )) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐽)) & ⊢ (𝜑 → 𝑇 ∈ (Clsd‘𝐽)) & ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇)) → if(1 ≤ (𝐹‘𝐵), 1, (𝐹‘𝐵)) ≤ (𝐴𝐷𝐵)) | ||
| Theorem | metnrmlem2 24895* | Lemma for metnrm 24897. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Mario Carneiro, 5-Sep-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < )) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐽)) & ⊢ (𝜑 → 𝑇 ∈ (Clsd‘𝐽)) & ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅) & ⊢ 𝑈 = ∪ 𝑡 ∈ 𝑇 (𝑡(ball‘𝐷)(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2)) ⇒ ⊢ (𝜑 → (𝑈 ∈ 𝐽 ∧ 𝑇 ⊆ 𝑈)) | ||
| Theorem | metnrmlem3 24896* | Lemma for metnrm 24897. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Mario Carneiro, 5-Sep-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < )) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐽)) & ⊢ (𝜑 → 𝑇 ∈ (Clsd‘𝐽)) & ⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅) & ⊢ 𝑈 = ∪ 𝑡 ∈ 𝑇 (𝑡(ball‘𝐷)(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2)) & ⊢ 𝐺 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑇 ↦ (𝑥𝐷𝑦)), ℝ*, < )) & ⊢ 𝑉 = ∪ 𝑠 ∈ 𝑆 (𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ⇒ ⊢ (𝜑 → ∃𝑧 ∈ 𝐽 ∃𝑤 ∈ 𝐽 (𝑆 ⊆ 𝑧 ∧ 𝑇 ⊆ 𝑤 ∧ (𝑧 ∩ 𝑤) = ∅)) | ||
| Theorem | metnrm 24897 | 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.) |
| ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Nrm) | ||
| Theorem | metreg 24898 | A metric space is regular. (Contributed by Mario Carneiro, 29-Dec-2016.) |
| ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Reg) | ||
| Theorem | addcnlem 24899* | Lemma for addcn 24900, subcn 24901, and mulcn 24902. (Contributed by Mario Carneiro, 5-May-2014.) (Proof shortened by Mario Carneiro, 2-Sep-2015.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ + :(ℂ × ℂ)⟶ℂ & ⊢ ((𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ) → ∃𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝑏)) < 𝑦 ∧ (abs‘(𝑣 − 𝑐)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝑏 + 𝑐))) < 𝑎)) ⇒ ⊢ + ∈ ((𝐽 ×t 𝐽) Cn 𝐽) | ||
| Theorem | addcn 24900 | 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.) |
| ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ + ∈ ((𝐽 ×t 𝐽) Cn 𝐽) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |