Home | Metamath
Proof Explorer Theorem List (p. 225 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | remet 22401 | The absolute value metric determines a metric space on the reals. (Contributed by NM, 10-Feb-2007.) |
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ 𝐷 ∈ (Met‘ℝ) | ||
Theorem | rexmet 22402 | The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015.) |
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ 𝐷 ∈ (∞Met‘ℝ) | ||
Theorem | bl2ioo 22403 | 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 22404 | 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 22405 | An open interval of reals in terms of a ball. (Contributed by Mario Carneiro, 14-Nov-2013.) |
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴(,)𝐵) ∈ ran (ball‘𝐷)) | ||
Theorem | blssioo 22406 | 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 22407 | 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 22408 | ℚ is dense in ℝ. (Contributed by NM, 24-Aug-2007.) |
⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((cls‘𝐽)‘ℚ) = ℝ | ||
Theorem | blcvx 22409 | 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 22410 | The standard topology on the reals is Hausdorff. (Contributed by NM, 8-Mar-2007.) |
⊢ (topGen‘ran (,)) ∈ Haus | ||
Theorem | tgqioo 22411 | 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 22412 | The standard topology on the reals is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ (topGen‘ran (,)) ∈ 2nd𝜔 | ||
Theorem | resubmet 22413 | 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 22414 | 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 22415 | 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 22416 | 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 22417 | 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 22418 | The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ 𝑋 = (ordTop‘ ≤ ) & ⊢ 𝑅 = (topGen‘ran (,)) ⇒ ⊢ (𝐴 ⊆ ℝ → (𝑋 ↾t 𝐴) = (𝑅 ↾t 𝐴)) | ||
Theorem | xrrest2 22419 | The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝑋 = (ordTop‘ ≤ ) ⇒ ⊢ (𝐴 ⊆ ℝ → (𝐽 ↾t 𝐴) = (𝑋 ↾t 𝐴)) | ||
Theorem | xrsxmet 22420 | The metric on the extended reals is a proper extended metric. (Contributed by Mario Carneiro, 4-Sep-2015.) |
⊢ 𝐷 = (dist‘ℝ*𝑠) ⇒ ⊢ 𝐷 ∈ (∞Met‘ℝ*) | ||
Theorem | xrsdsre 22421 | 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 22422 | 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 22423 | 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 22424 | The integers are a closed set in the topology on ℝ. (Contributed by Mario Carneiro, 17-Feb-2015.) |
⊢ 𝐽 = (topGen‘ran (,)) ⇒ ⊢ ℤ ∈ (Clsd‘𝐽) | ||
Theorem | recld2 22425 | The real numbers are a closed set in the topology on ℂ. (Contributed by Mario Carneiro, 17-Feb-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ ℝ ∈ (Clsd‘𝐽) | ||
Theorem | zcld2 22426 | The integers are a closed set in the topology on ℂ. (Contributed by Mario Carneiro, 17-Feb-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ ℤ ∈ (Clsd‘𝐽) | ||
Theorem | zdis 22427 | The integers are a discrete set in the topology on ℂ. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝐽 ↾t ℤ) = 𝒫 ℤ | ||
Theorem | sszcld 22428 | Every subset of the integers are closed in the topology on ℂ. (Contributed by Mario Carneiro, 6-Jul-2017.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝐴 ⊆ ℤ → 𝐴 ∈ (Clsd‘𝐽)) | ||
Theorem | reperflem 22429* | 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 22430 | The real numbers are a perfect subset of the complex numbers. (Contributed by Mario Carneiro, 26-Dec-2016.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝐽 ↾t ℝ) ∈ Perf | ||
Theorem | cnperf 22431 | The complex numbers are a perfect space. (Contributed by Mario Carneiro, 26-Dec-2016.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐽 ∈ Perf | ||
Theorem | iccntr 22432 | 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 22433* | Lemma for icccmp 22436. (Contributed by Mario Carneiro, 18-Jun-2014.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵)) & ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) & ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝑈 ⊆ 𝐽) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) ⇒ ⊢ (𝜑 → (𝐴 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵)) | ||
Theorem | icccmplem2 22434* | Lemma for icccmp 22436. (Contributed by Mario Carneiro, 13-Jun-2014.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵)) & ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) & ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝑈 ⊆ 𝐽) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) & ⊢ (𝜑 → 𝑉 ∈ 𝑈) & ⊢ (𝜑 → 𝐶 ∈ ℝ+) & ⊢ (𝜑 → (𝐺(ball‘𝐷)𝐶) ⊆ 𝑉) & ⊢ 𝐺 = sup(𝑆, ℝ, < ) & ⊢ 𝑅 = if((𝐺 + (𝐶 / 2)) ≤ 𝐵, (𝐺 + (𝐶 / 2)), 𝐵) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑆) | ||
Theorem | icccmplem3 22435* | Lemma for icccmp 22436. (Contributed by Mario Carneiro, 13-Jun-2014.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵)) & ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ)) & ⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) & ⊢ (𝜑 → 𝑈 ⊆ 𝐽) & ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑆) | ||
Theorem | icccmp 22436 | A closed interval in ℝ is compact. (Contributed by Mario Carneiro, 13-Jun-2014.) |
⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵)) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑇 ∈ Comp) | ||
Theorem | reconnlem1 22437 | Lemma for reconn 22439. Connectedness in the reals-easy direction. (Contributed by Jeff Hankins, 13-Jul-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.) |
⊢ (((𝐴 ⊆ ℝ ∧ ((topGen‘ran (,)) ↾t 𝐴) ∈ Con) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → (𝑋[,]𝑌) ⊆ 𝐴) | ||
Theorem | reconnlem2 22438* | Lemma for reconn 22439. (Contributed by Jeff Hankins, 17-Aug-2009.) (Proof shortened by Mario Carneiro, 9-Sep-2015.) |
⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝑈 ∈ (topGen‘ran (,))) & ⊢ (𝜑 → 𝑉 ∈ (topGen‘ran (,))) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ (𝑈 ∩ 𝐴)) & ⊢ (𝜑 → 𝐶 ∈ (𝑉 ∩ 𝐴)) & ⊢ (𝜑 → (𝑈 ∩ 𝑉) ⊆ (ℝ ∖ 𝐴)) & ⊢ (𝜑 → 𝐵 ≤ 𝐶) & ⊢ 𝑆 = sup((𝑈 ∩ (𝐵[,]𝐶)), ℝ, < ) ⇒ ⊢ (𝜑 → ¬ 𝐴 ⊆ (𝑈 ∪ 𝑉)) | ||
Theorem | reconn 22439* | 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 𝐴) ∈ Con ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥[,]𝑦) ⊆ 𝐴)) | ||
Theorem | retopcon 22440 | Corollary of reconn 22439. The set of real numbers is connected. (Contributed by Jeff Hankins, 17-Aug-2009.) |
⊢ (topGen‘ran (,)) ∈ Con | ||
Theorem | iccconn 22441 | A closed interval is connected. (Contributed by Jeff Hankins, 17-Aug-2009.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((topGen‘ran (,)) ↾t (𝐴[,]𝐵)) ∈ Con) | ||
Theorem | opnreen 22442 | Every nonempty open set is uncountable. (Contributed by Mario Carneiro, 26-Jul-2014.) (Revised by Mario Carneiro, 20-Feb-2015.) |
⊢ ((𝐴 ∈ (topGen‘ran (,)) ∧ 𝐴 ≠ ∅) → 𝐴 ≈ 𝒫 ℕ) | ||
Theorem | rectbntr0 22443 | A countable subset of the reals has empty interior. (Contributed by Mario Carneiro, 26-Jul-2014.) |
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ) → ((int‘(topGen‘ran (,)))‘𝐴) = ∅) | ||
Theorem | xrge0gsumle 22444 | 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 22445* | 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 22446 | 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 𝐹) ≈ 1𝑜) | ||
Theorem | metdcnlem 22447 | 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 22448 | The metric function of an extended metric space is always continuous in the topology generated by it. In this variation of xmetdcn 22449 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 22449 | 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 22450 | 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 22451 | 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 22452 | 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 22453* | Continuity of the metric function; analogue of cnmpt12f 21279 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 22454* | Continuity of the metric function; analogue of cnmpt22f 21288 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 22455 | 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 22456 | 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 22457 | 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 22458* | 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 22459* | 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 22460* | 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 22461* | 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 22462* | 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 22463* | 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 22464* | 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 22465* | 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 22466* | Lemma for metdscn 22467. (Contributed by Mario Carneiro, 4-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < )) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐶 = (dist‘ℝ*𝑠) & ⊢ 𝐾 = (MetOpen‘𝐶) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑆 ⊆ 𝑋) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → (𝐴𝐷𝐵) < 𝑅) ⇒ ⊢ (𝜑 → ((𝐹‘𝐴) +𝑒 -𝑒(𝐹‘𝐵)) < 𝑅) | ||
Theorem | metdscn 22467* | 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 22468* | 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 22469* | Lemma for metnrm 22473. (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 22470* | Lemma for metnrm 22473. (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 22471* | Lemma for metnrm 22473. (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 22472* | Lemma for metnrm 22473. (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 22473 | 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 22474 | A metric space is regular. (Contributed by Mario Carneiro, 29-Dec-2016.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Reg) | ||
Theorem | addcnlem 22475* | Lemma for addcn 22476, subcn 22477, and mulcn 22478. (Contributed by Mario Carneiro, 5-May-2014.) (Proof shortened by Mario Carneiro, 2-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ + :(ℂ × ℂ)⟶ℂ & ⊢ ((𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ) → ∃𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝑏)) < 𝑦 ∧ (abs‘(𝑣 − 𝑐)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝑏 + 𝑐))) < 𝑎)) ⇒ ⊢ + ∈ ((𝐽 ×t 𝐽) Cn 𝐽) | ||
Theorem | addcn 22476 | 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 𝐽) | ||
Theorem | subcn 22477 | 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.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ − ∈ ((𝐽 ×t 𝐽) Cn 𝐽) | ||
Theorem | mulcn 22478 | 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.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ · ∈ ((𝐽 ×t 𝐽) Cn 𝐽) | ||
Theorem | divcn 22479 | Complex number division is a continuous function, when the second argument is nonzero. (Contributed by Mario Carneiro, 12-Aug-2014.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (𝐽 ↾t (ℂ ∖ {0})) ⇒ ⊢ / ∈ ((𝐽 ×t 𝐾) Cn 𝐽) | ||
Theorem | cnfldtgp 22480 | The complex numbers form a topological group under addition, with the standard topology induced by the absolute value metric. (Contributed by Mario Carneiro, 2-Sep-2015.) |
⊢ ℂfld ∈ TopGrp | ||
Theorem | fsumcn 22481* | 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.) |
⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ (𝐽 Cn 𝐾)) | ||
Theorem | fsum2cn 22482* | Version of fsumcn 22481 for two-argument mappings. (Contributed by Mario Carneiro, 6-May-2014.) |
⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑌)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐽 ×t 𝐿) Cn 𝐾)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ ((𝐽 ×t 𝐿) Cn 𝐾)) | ||
Theorem | expcn 22483* | 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.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℂ ↦ (𝑥↑𝑁)) ∈ (𝐽 Cn 𝐽)) | ||
Theorem | divccn 22484* | Division by a nonzero constant is a continuous operation. (Contributed by Mario Carneiro, 5-May-2014.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / 𝐴)) ∈ (𝐽 Cn 𝐽)) | ||
Theorem | sqcn 22485* | The square function on complex numbers is continuous. (Contributed by NM, 13-Jun-2007.) (Proof shortened by Mario Carneiro, 5-May-2014.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝑥 ∈ ℂ ↦ (𝑥↑2)) ∈ (𝐽 Cn 𝐽) | ||
Syntax | cii 22486 | Extend class notation with the unit interval. |
class II | ||
Syntax | ccncf 22487 | Extend class notation to include the operation which returns a class of continuous complex functions. |
class –cn→ | ||
Definition | df-ii 22488 | Define the unit interval with the Euclidean topology. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 3-Sep-2015.) |
⊢ II = (MetOpen‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1)))) | ||
Definition | df-cncf 22489* | Define the operation whose value is a class of continuous complex functions. (Contributed by Paul Chapman, 11-Oct-2007.) |
⊢ –cn→ = (𝑎 ∈ 𝒫 ℂ, 𝑏 ∈ 𝒫 ℂ ↦ {𝑓 ∈ (𝑏 ↑𝑚 𝑎) ∣ ∀𝑥 ∈ 𝑎 ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑦 ∈ 𝑎 ((abs‘(𝑥 − 𝑦)) < 𝑑 → (abs‘((𝑓‘𝑥) − (𝑓‘𝑦))) < 𝑒)}) | ||
Theorem | iitopon 22490 | The unit interval is a topological space. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ II ∈ (TopOn‘(0[,]1)) | ||
Theorem | iitop 22491 | The unit interval is a topological space. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ II ∈ Top | ||
Theorem | iiuni 22492 | The base set of the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Jan-2014.) |
⊢ (0[,]1) = ∪ II | ||
Theorem | dfii2 22493 | Alternate definition of the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ II = ((topGen‘ran (,)) ↾t (0[,]1)) | ||
Theorem | dfii3 22494 | Alternate definition of the unit interval. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ II = (𝐽 ↾t (0[,]1)) | ||
Theorem | dfii4 22495 | Alternate definition of the unit interval. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐼 = (ℂfld ↾s (0[,]1)) ⇒ ⊢ II = (TopOpen‘𝐼) | ||
Theorem | dfii5 22496 | The unit interval expressed as an order topology. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ II = (ordTop‘( ≤ ∩ ((0[,]1) × (0[,]1)))) | ||
Theorem | iicmp 22497 | The unit interval is compact. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Jun-2014.) |
⊢ II ∈ Comp | ||
Theorem | iicon 22498 | The unit interval is connected. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ II ∈ Con | ||
Theorem | cncfval 22499* | 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.) |
⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐴–cn→𝐵) = {𝑓 ∈ (𝐵 ↑𝑚 𝐴) ∣ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝑓‘𝑥) − (𝑓‘𝑤))) < 𝑦)}) | ||
Theorem | elcncf 22500* | Membership in the set of continuous complex functions from 𝐴 to 𝐵. (Contributed by Paul Chapman, 11-Oct-2007.) (Revised by Mario Carneiro, 9-Nov-2013.) |
⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |