Home | Metamath
Proof Explorer Theorem List (p. 235 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | addcnlem 23401* | Lemma for addcn 23402, subcn 23403, and mulcn 23404. (Contributed by Mario Carneiro, 5-May-2014.) (Proof shortened by Mario Carneiro, 2-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ + :(ℂ × ℂ)⟶ℂ & ⊢ ((𝑎 ∈ ℝ+ ∧ 𝑏 ∈ ℂ ∧ 𝑐 ∈ ℂ) → ∃𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑢 ∈ ℂ ∀𝑣 ∈ ℂ (((abs‘(𝑢 − 𝑏)) < 𝑦 ∧ (abs‘(𝑣 − 𝑐)) < 𝑧) → (abs‘((𝑢 + 𝑣) − (𝑏 + 𝑐))) < 𝑎)) ⇒ ⊢ + ∈ ((𝐽 ×t 𝐽) Cn 𝐽) | ||
Theorem | addcn 23402 | 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 23403 | 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 23404 | 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 23405 | 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 23406 | 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 23407* | 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 23408* | Version of fsumcn 23407 for two-argument mappings. (Contributed by Mario Carneiro, 6-May-2014.) |
⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑌)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐽 ×t 𝐿) Cn 𝐾)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ ((𝐽 ×t 𝐿) Cn 𝐾)) | ||
Theorem | expcn 23409* | 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 23410* | Division by a nonzero constant is a continuous operation. (Contributed by Mario Carneiro, 5-May-2014.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / 𝐴)) ∈ (𝐽 Cn 𝐽)) | ||
Theorem | sqcn 23411* | 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 23412 | Extend class notation with the unit interval. |
class II | ||
Syntax | ccncf 23413 | Extend class notation to include the operation which returns a class of continuous complex functions. |
class –cn→ | ||
Definition | df-ii 23414 | 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 23415* | Define the operation whose value is a class of continuous complex functions. (Contributed by Paul Chapman, 11-Oct-2007.) |
⊢ –cn→ = (𝑎 ∈ 𝒫 ℂ, 𝑏 ∈ 𝒫 ℂ ↦ {𝑓 ∈ (𝑏 ↑m 𝑎) ∣ ∀𝑥 ∈ 𝑎 ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+ ∀𝑦 ∈ 𝑎 ((abs‘(𝑥 − 𝑦)) < 𝑑 → (abs‘((𝑓‘𝑥) − (𝑓‘𝑦))) < 𝑒)}) | ||
Theorem | iitopon 23416 | The unit interval is a topological space. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ II ∈ (TopOn‘(0[,]1)) | ||
Theorem | iitop 23417 | The unit interval is a topological space. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ II ∈ Top | ||
Theorem | iiuni 23418 | 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 23419 | Alternate definition of the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ II = ((topGen‘ran (,)) ↾t (0[,]1)) | ||
Theorem | dfii3 23420 | 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 23421 | Alternate definition of the unit interval. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐼 = (ℂfld ↾s (0[,]1)) ⇒ ⊢ II = (TopOpen‘𝐼) | ||
Theorem | dfii5 23422 | The unit interval expressed as an order topology. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ II = (ordTop‘( ≤ ∩ ((0[,]1) × (0[,]1)))) | ||
Theorem | iicmp 23423 | The unit interval is compact. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Jun-2014.) |
⊢ II ∈ Comp | ||
Theorem | iiconn 23424 | The unit interval is connected. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ II ∈ Conn | ||
Theorem | cncfval 23425* | 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→𝐵) = {𝑓 ∈ (𝐵 ↑m 𝐴) ∣ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑥 − 𝑤)) < 𝑧 → (abs‘((𝑓‘𝑥) − (𝑓‘𝑤))) < 𝑦)}) | ||
Theorem | elcncf 23426* | 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‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)))) | ||
Theorem | elcncf2 23427* | Version of elcncf 23426 with arguments commuted. (Contributed by Mario Carneiro, 28-Apr-2014.) |
⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑦)))) | ||
Theorem | cncfrss 23428 | Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ) | ||
Theorem | cncfrss2 23429 | Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ) | ||
Theorem | cncff 23430 | A continuous complex function's domain and codomain. (Contributed by Paul Chapman, 17-Jan-2008.) (Revised by Mario Carneiro, 25-Aug-2014.) |
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐹:𝐴⟶𝐵) | ||
Theorem | cncfi 23431* | Defining property of a continuous function. (Contributed by Mario Carneiro, 30-Apr-2014.) (Revised by Mario Carneiro, 25-Aug-2014.) |
⊢ ((𝐹 ∈ (𝐴–cn→𝐵) ∧ 𝐶 ∈ 𝐴 ∧ 𝑅 ∈ ℝ+) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝐶))) < 𝑅)) | ||
Theorem | elcncf1di 23432* | Membership in the set of continuous complex functions from 𝐴 to 𝐵. (Contributed by Paul Chapman, 26-Nov-2007.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+) → 𝑍 ∈ ℝ+)) & ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ ℝ+) → ((abs‘(𝑥 − 𝑤)) < 𝑍 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))) ⇒ ⊢ (𝜑 → ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → 𝐹 ∈ (𝐴–cn→𝐵))) | ||
Theorem | elcncf1ii 23433* | Membership in the set of continuous complex functions from 𝐴 to 𝐵. (Contributed by Paul Chapman, 26-Nov-2007.) |
⊢ 𝐹:𝐴⟶𝐵 & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+) → 𝑍 ∈ ℝ+) & ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ ℝ+) → ((abs‘(𝑥 − 𝑤)) < 𝑍 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)) ⇒ ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → 𝐹 ∈ (𝐴–cn→𝐵)) | ||
Theorem | rescncf 23434 | A continuous complex function restricted to a subset is continuous. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 25-Aug-2014.) |
⊢ (𝐶 ⊆ 𝐴 → (𝐹 ∈ (𝐴–cn→𝐵) → (𝐹 ↾ 𝐶) ∈ (𝐶–cn→𝐵))) | ||
Theorem | cncffvrn 23435 | Change the codomain of a continuous complex function. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 1-May-2015.) |
⊢ ((𝐶 ⊆ ℂ ∧ 𝐹 ∈ (𝐴–cn→𝐵)) → (𝐹 ∈ (𝐴–cn→𝐶) ↔ 𝐹:𝐴⟶𝐶)) | ||
Theorem | cncfss 23436 | The set of continuous functions is expanded when the range is expanded. (Contributed by Mario Carneiro, 30-Aug-2014.) |
⊢ ((𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ℂ) → (𝐴–cn→𝐵) ⊆ (𝐴–cn→𝐶)) | ||
Theorem | climcncf 23437 | Image of a limit under a continuous map. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵)) & ⊢ (𝜑 → 𝐺:𝑍⟶𝐴) & ⊢ (𝜑 → 𝐺 ⇝ 𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐺) ⇝ (𝐹‘𝐷)) | ||
Theorem | abscncf 23438 | Absolute value is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
⊢ abs ∈ (ℂ–cn→ℝ) | ||
Theorem | recncf 23439 | Real part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
⊢ ℜ ∈ (ℂ–cn→ℝ) | ||
Theorem | imcncf 23440 | Imaginary part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
⊢ ℑ ∈ (ℂ–cn→ℝ) | ||
Theorem | cjcncf 23441 | Complex conjugate is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
⊢ ∗ ∈ (ℂ–cn→ℂ) | ||
Theorem | mulc1cncf 23442* | Multiplication by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)) ⇒ ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ)) | ||
Theorem | divccncf 23443* | Division by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) |
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝑥 / 𝐴)) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 𝐹 ∈ (ℂ–cn→ℂ)) | ||
Theorem | cncfco 23444 | 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.) |
⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵)) & ⊢ (𝜑 → 𝐺 ∈ (𝐵–cn→𝐶)) ⇒ ⊢ (𝜑 → (𝐺 ∘ 𝐹) ∈ (𝐴–cn→𝐶)) | ||
Theorem | cncfmet 23445 | Relate complex function continuity to metric space continuity. (Contributed by Paul Chapman, 26-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.) |
⊢ 𝐶 = ((abs ∘ − ) ↾ (𝐴 × 𝐴)) & ⊢ 𝐷 = ((abs ∘ − ) ↾ (𝐵 × 𝐵)) & ⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐴–cn→𝐵) = (𝐽 Cn 𝐾)) | ||
Theorem | cncfcn 23446 | Relate complex function continuity to topological continuity. (Contributed by Mario Carneiro, 17-Feb-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (𝐽 ↾t 𝐴) & ⊢ 𝐿 = (𝐽 ↾t 𝐵) ⇒ ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐴–cn→𝐵) = (𝐾 Cn 𝐿)) | ||
Theorem | cncfcn1 23447 | Relate complex function continuity to topological continuity. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (ℂ–cn→ℂ) = (𝐽 Cn 𝐽) | ||
Theorem | cncfmptc 23448* | A constant function is a continuous function on ℂ. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Sep-2015.) |
⊢ ((𝐴 ∈ 𝑇 ∧ 𝑆 ⊆ ℂ ∧ 𝑇 ⊆ ℂ) → (𝑥 ∈ 𝑆 ↦ 𝐴) ∈ (𝑆–cn→𝑇)) | ||
Theorem | cncfmptid 23449* | The identity function is a continuous function on ℂ. (Contributed by Jeff Madsen, 11-Jun-2010.) (Revised by Mario Carneiro, 17-May-2016.) |
⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → (𝑥 ∈ 𝑆 ↦ 𝑥) ∈ (𝑆–cn→𝑇)) | ||
Theorem | cncfmpt1f 23450* | Composition of continuous functions. –cn→ analogue of cnmpt11f 22202. (Contributed by Mario Carneiro, 3-Sep-2014.) |
⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐹‘𝐴)) ∈ (𝑋–cn→ℂ)) | ||
Theorem | cncfmpt2f 23451* | Composition of continuous functions. –cn→ analogue of cnmpt12f 22204. (Contributed by Mario Carneiro, 3-Sep-2014.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴𝐹𝐵)) ∈ (𝑋–cn→ℂ)) | ||
Theorem | cncfmpt2ss 23452* | Composition of continuous functions in a subset. (Contributed by Mario Carneiro, 17-May-2016.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→𝑆)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→𝑆)) & ⊢ 𝑆 ⊆ ℂ & ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴𝐹𝐵)) ∈ (𝑋–cn→𝑆)) | ||
Theorem | addccncf 23453* | Adding a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝑥 + 𝐴)) ⇒ ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ)) | ||
Theorem | cdivcncf 23454* | Division with a constant numerator is continuous. (Contributed by Mario Carneiro, 28-Dec-2016.) |
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥)) ⇒ ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ ((ℂ ∖ {0})–cn→ℂ)) | ||
Theorem | negcncf 23455* | The negative function is continuous. (Contributed by Mario Carneiro, 30-Dec-2016.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ -𝑥) ⇒ ⊢ (𝐴 ⊆ ℂ → 𝐹 ∈ (𝐴–cn→ℂ)) | ||
Theorem | negfcncf 23456* | The negative of a continuous complex function is continuous. (Contributed by Paul Chapman, 21-Jan-2008.) (Revised by Mario Carneiro, 25-Aug-2014.) |
⊢ 𝐺 = (𝑥 ∈ 𝐴 ↦ -(𝐹‘𝑥)) ⇒ ⊢ (𝐹 ∈ (𝐴–cn→ℂ) → 𝐺 ∈ (𝐴–cn→ℂ)) | ||
Theorem | abscncfALT 23457 | Absolute value is continuous. Alternate proof of abscncf 23438. (Contributed by NM, 6-Jun-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ abs ∈ (ℂ–cn→ℝ) | ||
Theorem | cncfcnvcn 23458 | Rewrite cmphaushmeo 22338 for functions on the complex numbers. (Contributed by Mario Carneiro, 19-Feb-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (𝐽 ↾t 𝑋) ⇒ ⊢ ((𝐾 ∈ Comp ∧ 𝐹 ∈ (𝑋–cn→𝑌)) → (𝐹:𝑋–1-1-onto→𝑌 ↔ ◡𝐹 ∈ (𝑌–cn→𝑋))) | ||
Theorem | expcncf 23459* | The power function on complex numbers, for fixed exponent N, is continuous. Similar to expcn 23409. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℂ ↦ (𝑥↑𝑁)) ∈ (ℂ–cn→ℂ)) | ||
Theorem | cnmptre 23460* | Lemma for iirevcn 23463 and related functions. (Contributed by Mario Carneiro, 6-Jun-2014.) |
⊢ 𝑅 = (TopOpen‘ℂfld) & ⊢ 𝐽 = ((topGen‘ran (,)) ↾t 𝐴) & ⊢ 𝐾 = ((topGen‘ran (,)) ↾t 𝐵) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐵 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 𝐹) ∈ (𝑅 Cn 𝑅)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐹) ∈ (𝐽 Cn 𝐾)) | ||
Theorem | cnmpopc 23461* | Piecewise definition of a continuous function on a real interval. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Jun-2014.) |
⊢ 𝑅 = (topGen‘ran (,)) & ⊢ 𝑀 = (𝑅 ↾t (𝐴[,]𝐵)) & ⊢ 𝑁 = (𝑅 ↾t (𝐵[,]𝐶)) & ⊢ 𝑂 = (𝑅 ↾t (𝐴[,]𝐶)) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐶)) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ ((𝜑 ∧ (𝑥 = 𝐵 ∧ 𝑦 ∈ 𝑋)) → 𝐷 = 𝐸) & ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐵), 𝑦 ∈ 𝑋 ↦ 𝐷) ∈ ((𝑀 ×t 𝐽) Cn 𝐾)) & ⊢ (𝜑 → (𝑥 ∈ (𝐵[,]𝐶), 𝑦 ∈ 𝑋 ↦ 𝐸) ∈ ((𝑁 ×t 𝐽) Cn 𝐾)) ⇒ ⊢ (𝜑 → (𝑥 ∈ (𝐴[,]𝐶), 𝑦 ∈ 𝑋 ↦ if(𝑥 ≤ 𝐵, 𝐷, 𝐸)) ∈ ((𝑂 ×t 𝐽) Cn 𝐾)) | ||
Theorem | iirev 23462 | Reverse the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑋 ∈ (0[,]1) → (1 − 𝑋) ∈ (0[,]1)) | ||
Theorem | iirevcn 23463 | The reversion function is a continuous map of the unit interval. (Contributed by Mario Carneiro, 6-Jun-2014.) |
⊢ (𝑥 ∈ (0[,]1) ↦ (1 − 𝑥)) ∈ (II Cn II) | ||
Theorem | iihalf1 23464 | Map the first half of II into II. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑋 ∈ (0[,](1 / 2)) → (2 · 𝑋) ∈ (0[,]1)) | ||
Theorem | iihalf1cn 23465 | The first half function is a continuous map. (Contributed by Mario Carneiro, 6-Jun-2014.) |
⊢ 𝐽 = ((topGen‘ran (,)) ↾t (0[,](1 / 2))) ⇒ ⊢ (𝑥 ∈ (0[,](1 / 2)) ↦ (2 · 𝑥)) ∈ (𝐽 Cn II) | ||
Theorem | iihalf2 23466 | Map the second half of II into II. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑋 ∈ ((1 / 2)[,]1) → ((2 · 𝑋) − 1) ∈ (0[,]1)) | ||
Theorem | iihalf2cn 23467 | The second half function is a continuous map. (Contributed by Mario Carneiro, 6-Jun-2014.) |
⊢ 𝐽 = ((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ⇒ ⊢ (𝑥 ∈ ((1 / 2)[,]1) ↦ ((2 · 𝑥) − 1)) ∈ (𝐽 Cn II) | ||
Theorem | elii1 23468 | Divide the unit interval into two pieces. (Contributed by Mario Carneiro, 7-Jun-2014.) |
⊢ (𝑋 ∈ (0[,](1 / 2)) ↔ (𝑋 ∈ (0[,]1) ∧ 𝑋 ≤ (1 / 2))) | ||
Theorem | elii2 23469 | Divide the unit interval into two pieces. (Contributed by Mario Carneiro, 7-Jun-2014.) |
⊢ ((𝑋 ∈ (0[,]1) ∧ ¬ 𝑋 ≤ (1 / 2)) → 𝑋 ∈ ((1 / 2)[,]1)) | ||
Theorem | iimulcl 23470 | The unit interval is closed under multiplication. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐴 ∈ (0[,]1) ∧ 𝐵 ∈ (0[,]1)) → (𝐴 · 𝐵) ∈ (0[,]1)) | ||
Theorem | iimulcn 23471* | Multiplication is a continuous function on the unit interval. (Contributed by Mario Carneiro, 8-Jun-2014.) |
⊢ (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝑥 · 𝑦)) ∈ ((II ×t II) Cn II) | ||
Theorem | icoopnst 23472 | A half-open interval starting at 𝐴 is open in the closed interval from 𝐴 to 𝐵. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
⊢ 𝐽 = (MetOpen‘((abs ∘ − ) ↾ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴(,]𝐵) → (𝐴[,)𝐶) ∈ 𝐽)) | ||
Theorem | iocopnst 23473 | A half-open interval ending at 𝐵 is open in the closed interval from 𝐴 to 𝐵. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) |
⊢ 𝐽 = (MetOpen‘((abs ∘ − ) ↾ ((𝐴[,]𝐵) × (𝐴[,]𝐵)))) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,)𝐵) → (𝐶(,]𝐵) ∈ 𝐽)) | ||
Theorem | icchmeo 23474* | The natural bijection from [0, 1] to an arbitrary nontrivial closed interval [𝐴, 𝐵] is a homeomorphism. (Contributed by Mario Carneiro, 8-Sep-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴))) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐹 ∈ (IIHomeo(𝐽 ↾t (𝐴[,]𝐵)))) | ||
Theorem | icopnfcnv 23475* | Define a bijection from [0, 1) to [0, +∞). (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥))) ⇒ ⊢ (𝐹:(0[,)1)–1-1-onto→(0[,)+∞) ∧ ◡𝐹 = (𝑦 ∈ (0[,)+∞) ↦ (𝑦 / (1 + 𝑦)))) | ||
Theorem | icopnfhmeo 23476* | The defined bijection from [0, 1) to [0, +∞) is an order isomorphism and a homeomorphism. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ (0[,)1) ↦ (𝑥 / (1 − 𝑥))) & ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝐹 Isom < , < ((0[,)1), (0[,)+∞)) ∧ 𝐹 ∈ ((𝐽 ↾t (0[,)1))Homeo(𝐽 ↾t (0[,)+∞)))) | ||
Theorem | iccpnfcnv 23477* | Define a bijection from [0, 1] to [0, +∞]. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥)))) ⇒ ⊢ (𝐹:(0[,]1)–1-1-onto→(0[,]+∞) ∧ ◡𝐹 = (𝑦 ∈ (0[,]+∞) ↦ if(𝑦 = +∞, 1, (𝑦 / (1 + 𝑦))))) | ||
Theorem | iccpnfhmeo 23478 | The defined bijection from [0, 1] to [0, +∞] is an order isomorphism and a homeomorphism. (Contributed by Mario Carneiro, 8-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥)))) & ⊢ 𝐾 = ((ordTop‘ ≤ ) ↾t (0[,]+∞)) ⇒ ⊢ (𝐹 Isom < , < ((0[,]1), (0[,]+∞)) ∧ 𝐹 ∈ (IIHomeo𝐾)) | ||
Theorem | xrhmeo 23479* | The bijection from [-1, 1] to the extended reals is an order isomorphism and a homeomorphism. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ if(𝑥 = 1, +∞, (𝑥 / (1 − 𝑥)))) & ⊢ 𝐺 = (𝑦 ∈ (-1[,]1) ↦ if(0 ≤ 𝑦, (𝐹‘𝑦), -𝑒(𝐹‘-𝑦))) & ⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝐺 Isom < , < ((-1[,]1), ℝ*) ∧ 𝐺 ∈ ((𝐽 ↾t (-1[,]1))Homeo(ordTop‘ ≤ ))) | ||
Theorem | xrhmph 23480 | The extended reals are homeomorphic to the interval [0, 1]. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ II ≃ (ordTop‘ ≤ ) | ||
Theorem | xrcmp 23481 | The topology of the extended reals is compact. Since the topology of the extended reals extends the topology of the reals (by xrtgioo 23343), this means that ℝ* is a compactification of ℝ. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ (ordTop‘ ≤ ) ∈ Comp | ||
Theorem | xrconn 23482 | The topology of the extended reals is connected. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ (ordTop‘ ≤ ) ∈ Conn | ||
Theorem | icccvx 23483 | A linear combination of two reals lies in the interval between them. Equivalently, a closed interval is a convex set. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐶 ∈ (𝐴[,]𝐵) ∧ 𝐷 ∈ (𝐴[,]𝐵) ∧ 𝑇 ∈ (0[,]1)) → (((1 − 𝑇) · 𝐶) + (𝑇 · 𝐷)) ∈ (𝐴[,]𝐵))) | ||
Theorem | oprpiece1res1 23484* | Restriction to the first part of a piecewise defined function. (Contributed by Jeff Madsen, 11-Jun-2010.) (Proof shortened by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐴 ≤ 𝐵 & ⊢ 𝑅 ∈ V & ⊢ 𝑆 ∈ V & ⊢ 𝐾 ∈ (𝐴[,]𝐵) & ⊢ 𝐹 = (𝑥 ∈ (𝐴[,]𝐵), 𝑦 ∈ 𝐶 ↦ if(𝑥 ≤ 𝐾, 𝑅, 𝑆)) & ⊢ 𝐺 = (𝑥 ∈ (𝐴[,]𝐾), 𝑦 ∈ 𝐶 ↦ 𝑅) ⇒ ⊢ (𝐹 ↾ ((𝐴[,]𝐾) × 𝐶)) = 𝐺 | ||
Theorem | oprpiece1res2 23485* | Restriction to the second part of a piecewise defined function. (Contributed by Jeff Madsen, 11-Jun-2010.) (Proof shortened by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐴 ∈ ℝ & ⊢ 𝐵 ∈ ℝ & ⊢ 𝐴 ≤ 𝐵 & ⊢ 𝑅 ∈ V & ⊢ 𝑆 ∈ V & ⊢ 𝐾 ∈ (𝐴[,]𝐵) & ⊢ 𝐹 = (𝑥 ∈ (𝐴[,]𝐵), 𝑦 ∈ 𝐶 ↦ if(𝑥 ≤ 𝐾, 𝑅, 𝑆)) & ⊢ (𝑥 = 𝐾 → 𝑅 = 𝑃) & ⊢ (𝑥 = 𝐾 → 𝑆 = 𝑄) & ⊢ (𝑦 ∈ 𝐶 → 𝑃 = 𝑄) & ⊢ 𝐺 = (𝑥 ∈ (𝐾[,]𝐵), 𝑦 ∈ 𝐶 ↦ 𝑆) ⇒ ⊢ (𝐹 ↾ ((𝐾[,]𝐵) × 𝐶)) = 𝐺 | ||
Theorem | cnrehmeo 23486* | The canonical bijection from (ℝ × ℝ) to ℂ described in cnref1o 12374 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.) |
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐹 ∈ ((𝐽 ×t 𝐽)Homeo𝐾) | ||
Theorem | cnheiborlem 23487* | Lemma for cnheibor 23488. (Contributed by Mario Carneiro, 14-Sep-2014.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝑇 = (𝐽 ↾t 𝑋) & ⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) & ⊢ 𝑌 = (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ⇒ ⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑇 ∈ Comp) | ||
Theorem | cnheibor 23488* | Heine-Borel theorem for complex numbers. A subset of ℂ is compact iff it is closed and bounded. (Contributed by Mario Carneiro, 14-Sep-2014.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝑇 = (𝐽 ↾t 𝑋) ⇒ ⊢ (𝑋 ⊆ ℂ → (𝑇 ∈ Comp ↔ (𝑋 ∈ (Clsd‘𝐽) ∧ ∃𝑟 ∈ ℝ ∀𝑥 ∈ 𝑋 (abs‘𝑥) ≤ 𝑟))) | ||
Theorem | cnllycmp 23489 | The topology on the complex numbers is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐽 ∈ 𝑛-Locally Comp | ||
Theorem | rellycmp 23490 | The topology on the reals is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ (topGen‘ran (,)) ∈ 𝑛-Locally Comp | ||
Theorem | bndth 23491* | The Boundedness Theorem. A continuous function from a compact topological space to the reals is bounded (above). (Boundedness below is obtained by applying this theorem to -𝐹.) (Contributed by Mario Carneiro, 12-Aug-2014.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐽 ∈ Comp) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ 𝑥) | ||
Theorem | evth 23492* | The Extreme Value Theorem. A continuous function from a nonempty compact topological space to the reals attains its maximum at some point in the domain. (Contributed by Mario Carneiro, 12-Aug-2014.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐽 ∈ Comp) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝑋 ≠ ∅) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ (𝐹‘𝑥)) | ||
Theorem | evth2 23493* | The Extreme Value Theorem, minimum version. A continuous function from a nonempty compact topological space to the reals attains its minimum at some point in the domain. (Contributed by Mario Carneiro, 12-Aug-2014.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐾 = (topGen‘ran (,)) & ⊢ (𝜑 → 𝐽 ∈ Comp) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝑋 ≠ ∅) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝐹‘𝑥) ≤ (𝐹‘𝑦)) | ||
Theorem | lebnumlem1 23494* | Lemma for lebnum 23497. The function 𝐹 measures the sum of all of the distances to escape the sets of the cover. Since by assumption it is a cover, there is at least one set which covers a given point, and since it is open, the point is a positive distance from the edge of the set. Thus, the sum is a strictly positive number. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by AV, 30-Sep-2020.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐽 ∈ Comp) & ⊢ (𝜑 → 𝑈 ⊆ 𝐽) & ⊢ (𝜑 → 𝑋 = ∪ 𝑈) & ⊢ (𝜑 → 𝑈 ∈ Fin) & ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈) & ⊢ 𝐹 = (𝑦 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < )) ⇒ ⊢ (𝜑 → 𝐹:𝑋⟶ℝ+) | ||
Theorem | lebnumlem2 23495* | Lemma for lebnum 23497. As a finite sum of point-to-set distance functions, which are continuous by metdscn 23393, the function 𝐹 is also continuous. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by AV, 30-Sep-2020.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐽 ∈ Comp) & ⊢ (𝜑 → 𝑈 ⊆ 𝐽) & ⊢ (𝜑 → 𝑋 = ∪ 𝑈) & ⊢ (𝜑 → 𝑈 ∈ Fin) & ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈) & ⊢ 𝐹 = (𝑦 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < )) & ⊢ 𝐾 = (topGen‘ran (,)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) | ||
Theorem | lebnumlem3 23496* | Lemma for lebnum 23497. By the previous lemmas, 𝐹 is continuous and positive on a compact set, so it has a positive minimum 𝑟. Then setting 𝑑 = 𝑟 / ♯(𝑈), since for each 𝑢 ∈ 𝑈 we have ball(𝑥, 𝑑) ⊆ 𝑢 iff 𝑑 ≤ 𝑑(𝑥, 𝑋 ∖ 𝑢), if ¬ ball(𝑥, 𝑑) ⊆ 𝑢 for all 𝑢 then summing over 𝑢 yields Σ𝑢 ∈ 𝑈𝑑(𝑥, 𝑋 ∖ 𝑢) = 𝐹(𝑥) < Σ𝑢 ∈ 𝑈𝑑 = 𝑟, in contradiction to the assumption that 𝑟 is the minimum of 𝐹. (Contributed by Mario Carneiro, 14-Feb-2015.) (Revised by Mario Carneiro, 5-Sep-2015.) (Revised by AV, 30-Sep-2020.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐽 ∈ Comp) & ⊢ (𝜑 → 𝑈 ⊆ 𝐽) & ⊢ (𝜑 → 𝑋 = ∪ 𝑈) & ⊢ (𝜑 → 𝑈 ∈ Fin) & ⊢ (𝜑 → ¬ 𝑋 ∈ 𝑈) & ⊢ 𝐹 = (𝑦 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝑈 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < )) & ⊢ 𝐾 = (topGen‘ran (,)) ⇒ ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) | ||
Theorem | lebnum 23497* | The Lebesgue number lemma, or Lebesgue covering lemma. If 𝑋 is a compact metric space and 𝑈 is an open cover of 𝑋, then there exists a positive real number 𝑑 such that every ball of size 𝑑 (and every subset of a ball of size 𝑑, including every subset of diameter less than 𝑑) is a subset of some member of the cover. (Contributed by Mario Carneiro, 14-Feb-2015.) (Proof shortened by Mario Carneiro, 5-Sep-2015.) (Proof shortened by AV, 30-Sep-2020.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐽 ∈ Comp) & ⊢ (𝜑 → 𝑈 ⊆ 𝐽) & ⊢ (𝜑 → 𝑋 = ∪ 𝑈) ⇒ ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) | ||
Theorem | xlebnum 23498* | Generalize lebnum 23497 to extended metrics. (Contributed by Mario Carneiro, 5-Sep-2015.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝐽 ∈ Comp) & ⊢ (𝜑 → 𝑈 ⊆ 𝐽) & ⊢ (𝜑 → 𝑋 = ∪ 𝑈) ⇒ ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) | ||
Theorem | lebnumii 23499* | Specialize the Lebesgue number lemma lebnum 23497 to the closed unit interval. (Contributed by Mario Carneiro, 14-Feb-2015.) |
⊢ ((𝑈 ⊆ II ∧ (0[,]1) = ∪ 𝑈) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (1...𝑛)∃𝑢 ∈ 𝑈 (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑢) | ||
Syntax | chtpy 23500 | Extend class notation with the class of homotopies between two continuous functions. |
class Htpy |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |