![]() |
Metamath
Proof Explorer Theorem List (p. 250 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: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | subcn 24901 | 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 24902 | 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.) Usage of this theorem is discouraged because it depends on ax-mulf 11232. Use mpomulcn 24904 instead. (New usage is discouraged.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ · ∈ ((𝐽 ×t 𝐽) Cn 𝐽) | ||
Theorem | divcnOLD 24903 | Obsolete version of divcn 24905 as of 6-Apr-2025. (Contributed by Mario Carneiro, 12-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (𝐽 ↾t (ℂ ∖ {0})) ⇒ ⊢ / ∈ ((𝐽 ×t 𝐾) Cn 𝐽) | ||
Theorem | mpomulcn 24904* | Complex number multiplication is a continuous function. Version of mulcn 24902 using maps-to notation, which does not require ax-mulf 11232. (Contributed by GG, 16-Mar-2025.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽) | ||
Theorem | divcn 24905 | Complex number division is a continuous function, when the second argument is nonzero. (Contributed by Mario Carneiro, 12-Aug-2014.) Avoid ax-mulf 11232. (Revised by GG, 16-Mar-2025.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (𝐽 ↾t (ℂ ∖ {0})) ⇒ ⊢ / ∈ ((𝐽 ×t 𝐾) Cn 𝐽) | ||
Theorem | cnfldtgp 24906 | 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 24907* | 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 24908* | Version of fsumcn 24907 for two-argument mappings. (Contributed by Mario Carneiro, 6-May-2014.) |
⊢ 𝐾 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑌)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐽 ×t 𝐿) Cn 𝐾)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ Σ𝑘 ∈ 𝐴 𝐵) ∈ ((𝐽 ×t 𝐿) Cn 𝐾)) | ||
Theorem | expcn 24909* | 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.) Avoid ax-mulf 11232. (Revised by GG, 16-Mar-2025.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℂ ↦ (𝑥↑𝑁)) ∈ (𝐽 Cn 𝐽)) | ||
Theorem | divccn 24910* | Division by a nonzero constant is a continuous operation. (Contributed by Mario Carneiro, 5-May-2014.) Avoid ax-mulf 11232. (Revised by GG, 16-Mar-2025.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / 𝐴)) ∈ (𝐽 Cn 𝐽)) | ||
Theorem | expcnOLD 24911* | Obsolete version of expcn 24909 as of 6-Apr-2025. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 23-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℂ ↦ (𝑥↑𝑁)) ∈ (𝐽 Cn 𝐽)) | ||
Theorem | divccnOLD 24912* | Obsolete version of divccn 24910 as of 6-Apr-2025. (Contributed by Mario Carneiro, 5-May-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / 𝐴)) ∈ (𝐽 Cn 𝐽)) | ||
Theorem | sqcn 24913* | 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 24914 | Extend class notation with the unit interval. |
class II | ||
Syntax | ccncf 24915 | Extend class notation to include the operation which returns a class of continuous complex functions. |
class –cn→ | ||
Definition | df-ii 24916 | 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 24917* | 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 24918 | The unit interval is a topological space. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ II ∈ (TopOn‘(0[,]1)) | ||
Theorem | iitop 24919 | The unit interval is a topological space. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ II ∈ Top | ||
Theorem | iiuni 24920 | 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 24921 | Alternate definition of the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ II = ((topGen‘ran (,)) ↾t (0[,]1)) | ||
Theorem | dfii3 24922 | 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 24923 | Alternate definition of the unit interval. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ 𝐼 = (ℂfld ↾s (0[,]1)) ⇒ ⊢ II = (TopOpen‘𝐼) | ||
Theorem | dfii5 24924 | The unit interval expressed as an order topology. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ II = (ordTop‘( ≤ ∩ ((0[,]1) × (0[,]1)))) | ||
Theorem | iicmp 24925 | The unit interval is compact. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Jun-2014.) |
⊢ II ∈ Comp | ||
Theorem | iiconn 24926 | The unit interval is connected. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ II ∈ Conn | ||
Theorem | cncfval 24927* | 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 24928* | 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 24929* | Version of elcncf 24928 with arguments commuted. (Contributed by Mario Carneiro, 28-Apr-2014.) |
⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐹 ∈ (𝐴–cn→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((abs‘(𝑤 − 𝑥)) < 𝑧 → (abs‘((𝐹‘𝑤) − (𝐹‘𝑥))) < 𝑦)))) | ||
Theorem | cncfrss 24930 | Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ) | ||
Theorem | cncfrss2 24931 | Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ) | ||
Theorem | cncff 24932 | 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 24933* | 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 24934* | Membership in the set of continuous complex functions from 𝐴 to 𝐵. (Contributed by Paul Chapman, 26-Nov-2007.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+) → 𝑍 ∈ ℝ+)) & ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ ℝ+) → ((abs‘(𝑥 − 𝑤)) < 𝑍 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))) ⇒ ⊢ (𝜑 → ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → 𝐹 ∈ (𝐴–cn→𝐵))) | ||
Theorem | elcncf1ii 24935* | Membership in the set of continuous complex functions from 𝐴 to 𝐵. (Contributed by Paul Chapman, 26-Nov-2007.) |
⊢ 𝐹:𝐴⟶𝐵 & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+) → 𝑍 ∈ ℝ+) & ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ ℝ+) → ((abs‘(𝑥 − 𝑤)) < 𝑍 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)) ⇒ ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → 𝐹 ∈ (𝐴–cn→𝐵)) | ||
Theorem | rescncf 24936 | 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 | cncfcdm 24937 | 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 24938 | The set of continuous functions is expanded when the codomain is expanded. (Contributed by Mario Carneiro, 30-Aug-2014.) |
⊢ ((𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ℂ) → (𝐴–cn→𝐵) ⊆ (𝐴–cn→𝐶)) | ||
Theorem | climcncf 24939 | Image of a limit under a continuous map. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵)) & ⊢ (𝜑 → 𝐺:𝑍⟶𝐴) & ⊢ (𝜑 → 𝐺 ⇝ 𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐺) ⇝ (𝐹‘𝐷)) | ||
Theorem | abscncf 24940 | Absolute value is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
⊢ abs ∈ (ℂ–cn→ℝ) | ||
Theorem | recncf 24941 | Real part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
⊢ ℜ ∈ (ℂ–cn→ℝ) | ||
Theorem | imcncf 24942 | Imaginary part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
⊢ ℑ ∈ (ℂ–cn→ℝ) | ||
Theorem | cjcncf 24943 | Complex conjugate is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
⊢ ∗ ∈ (ℂ–cn→ℂ) | ||
Theorem | mulc1cncf 24944* | Multiplication by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)) ⇒ ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ)) | ||
Theorem | divccncf 24945* | Division by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) |
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝑥 / 𝐴)) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 𝐹 ∈ (ℂ–cn→ℂ)) | ||
Theorem | cncfco 24946 | 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 | cncfcompt2 24947* | Composition of continuous functions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ (𝐴–cn→𝐵)) & ⊢ (𝜑 → (𝑦 ∈ 𝐶 ↦ 𝑆) ∈ (𝐶–cn→𝐸)) & ⊢ (𝜑 → 𝐵 ⊆ 𝐶) & ⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑇) ∈ (𝐴–cn→𝐸)) | ||
Theorem | cncfmet 24948 | 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 24949 | Relate complex function continuity to topological continuity. (Contributed by Mario Carneiro, 17-Feb-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (𝐽 ↾t 𝐴) & ⊢ 𝐿 = (𝐽 ↾t 𝐵) ⇒ ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐴–cn→𝐵) = (𝐾 Cn 𝐿)) | ||
Theorem | cncfcn1 24950 | 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 24951* | 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 24952* | 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 24953* | Composition of continuous functions. –cn→ analogue of cnmpt11f 23687. (Contributed by Mario Carneiro, 3-Sep-2014.) |
⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐹‘𝐴)) ∈ (𝑋–cn→ℂ)) | ||
Theorem | cncfmpt2f 24954* | Composition of continuous functions. –cn→ analogue of cnmpt12f 23689. (Contributed by Mario Carneiro, 3-Sep-2014.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴𝐹𝐵)) ∈ (𝑋–cn→ℂ)) | ||
Theorem | cncfmpt2ss 24955* | Composition of continuous functions in a subset. (Contributed by Mario Carneiro, 17-May-2016.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→𝑆)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→𝑆)) & ⊢ 𝑆 ⊆ ℂ & ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴𝐹𝐵)) ∈ (𝑋–cn→𝑆)) | ||
Theorem | addccncf 24956* | Adding a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝑥 + 𝐴)) ⇒ ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ)) | ||
Theorem | idcncf 24957 | The identity function is a continuous function on ℂ. (Contributed by Jeff Madsen, 11-Jun-2010.) (Moved into main set.mm as cncfmptid 24952 and may be deleted by mathbox owner, JM. --MC 12-Sep-2015.) (Revised by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ 𝑥) ⇒ ⊢ 𝐹 ∈ (ℂ–cn→ℂ) | ||
Theorem | sub1cncf 24958* | Subtracting a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝑥 − 𝐴)) ⇒ ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ)) | ||
Theorem | sub2cncf 24959* | Subtraction from a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝐴 − 𝑥)) ⇒ ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ)) | ||
Theorem | cdivcncf 24960* | Division with a constant numerator is continuous. (Contributed by Mario Carneiro, 28-Dec-2016.) |
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥)) ⇒ ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ ((ℂ ∖ {0})–cn→ℂ)) | ||
Theorem | negcncf 24961* | The negative function is continuous. (Contributed by Mario Carneiro, 30-Dec-2016.) Avoid ax-mulf 11232. (Revised by GG, 16-Mar-2025.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ -𝑥) ⇒ ⊢ (𝐴 ⊆ ℂ → 𝐹 ∈ (𝐴–cn→ℂ)) | ||
Theorem | negcncfOLD 24962* | Obsolete version of negcncf 24961 as of 9-Apr-2025. (Contributed by Mario Carneiro, 30-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ -𝑥) ⇒ ⊢ (𝐴 ⊆ ℂ → 𝐹 ∈ (𝐴–cn→ℂ)) | ||
Theorem | negfcncf 24963* | 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 24964 | Absolute value is continuous. Alternate proof of abscncf 24940. (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 24965 | Rewrite cmphaushmeo 23823 for functions on the complex numbers. (Contributed by Mario Carneiro, 19-Feb-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (𝐽 ↾t 𝑋) ⇒ ⊢ ((𝐾 ∈ Comp ∧ 𝐹 ∈ (𝑋–cn→𝑌)) → (𝐹:𝑋–1-1-onto→𝑌 ↔ ◡𝐹 ∈ (𝑌–cn→𝑋))) | ||
Theorem | expcncf 24966* | The power function on complex numbers, for fixed exponent N, is continuous. Similar to expcn 24909. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℂ ↦ (𝑥↑𝑁)) ∈ (ℂ–cn→ℂ)) | ||
Theorem | cnmptre 24967* | Lemma for iirevcn 24970 and related functions. (Contributed by Mario Carneiro, 6-Jun-2014.) |
⊢ 𝑅 = (TopOpen‘ℂfld) & ⊢ 𝐽 = ((topGen‘ran (,)) ↾t 𝐴) & ⊢ 𝐾 = ((topGen‘ran (,)) ↾t 𝐵) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐵 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 𝐹) ∈ (𝑅 Cn 𝑅)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐹) ∈ (𝐽 Cn 𝐾)) | ||
Theorem | cnmpopc 24968* | 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 24969 | Reverse the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑋 ∈ (0[,]1) → (1 − 𝑋) ∈ (0[,]1)) | ||
Theorem | iirevcn 24970 | 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 24971 | Map the first half of II into II. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑋 ∈ (0[,](1 / 2)) → (2 · 𝑋) ∈ (0[,]1)) | ||
Theorem | iihalf1cn 24972 | The first half function is a continuous map. (Contributed by Mario Carneiro, 6-Jun-2014.) Avoid ax-mulf 11232. (Revised by GG, 16-Mar-2025.) |
⊢ 𝐽 = ((topGen‘ran (,)) ↾t (0[,](1 / 2))) ⇒ ⊢ (𝑥 ∈ (0[,](1 / 2)) ↦ (2 · 𝑥)) ∈ (𝐽 Cn II) | ||
Theorem | iihalf1cnOLD 24973 | Obsolete version of iihalf1cn 24972 as of 9-Apr-2025. (Contributed by Mario Carneiro, 6-Jun-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐽 = ((topGen‘ran (,)) ↾t (0[,](1 / 2))) ⇒ ⊢ (𝑥 ∈ (0[,](1 / 2)) ↦ (2 · 𝑥)) ∈ (𝐽 Cn II) | ||
Theorem | iihalf2 24974 | Map the second half of II into II. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑋 ∈ ((1 / 2)[,]1) → ((2 · 𝑋) − 1) ∈ (0[,]1)) | ||
Theorem | iihalf2cn 24975 | The second half function is a continuous map. (Contributed by Mario Carneiro, 6-Jun-2014.) Avoid ax-mulf 11232. (Revised by GG, 16-Mar-2025.) |
⊢ 𝐽 = ((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ⇒ ⊢ (𝑥 ∈ ((1 / 2)[,]1) ↦ ((2 · 𝑥) − 1)) ∈ (𝐽 Cn II) | ||
Theorem | iihalf2cnOLD 24976 | Obsolete version of iihalf2cn 24975 as of 9-Apr-2025. (Contributed by Mario Carneiro, 6-Jun-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐽 = ((topGen‘ran (,)) ↾t ((1 / 2)[,]1)) ⇒ ⊢ (𝑥 ∈ ((1 / 2)[,]1) ↦ ((2 · 𝑥) − 1)) ∈ (𝐽 Cn II) | ||
Theorem | elii1 24977 | Divide the unit interval into two pieces. (Contributed by Mario Carneiro, 7-Jun-2014.) |
⊢ (𝑋 ∈ (0[,](1 / 2)) ↔ (𝑋 ∈ (0[,]1) ∧ 𝑋 ≤ (1 / 2))) | ||
Theorem | elii2 24978 | Divide the unit interval into two pieces. (Contributed by Mario Carneiro, 7-Jun-2014.) |
⊢ ((𝑋 ∈ (0[,]1) ∧ ¬ 𝑋 ≤ (1 / 2)) → 𝑋 ∈ ((1 / 2)[,]1)) | ||
Theorem | iimulcl 24979 | The unit interval is closed under multiplication. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐴 ∈ (0[,]1) ∧ 𝐵 ∈ (0[,]1)) → (𝐴 · 𝐵) ∈ (0[,]1)) | ||
Theorem | iimulcn 24980* | Multiplication is a continuous function on the unit interval. (Contributed by Mario Carneiro, 8-Jun-2014.) Avoid ax-mulf 11232. (Revised by GG, 16-Mar-2025.) |
⊢ (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝑥 · 𝑦)) ∈ ((II ×t II) Cn II) | ||
Theorem | iimulcnOLD 24981* | Obsolete version of iimulcn 24980 as of 9-Apr-2025. (Contributed by Mario Carneiro, 8-Jun-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝑥 · 𝑦)) ∈ ((II ×t II) Cn II) | ||
Theorem | icoopnst 24982 | 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 24983 | 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 24984* | The natural bijection from [0, 1] to an arbitrary nontrivial closed interval [𝐴, 𝐵] is a homeomorphism. (Contributed by Mario Carneiro, 8-Sep-2015.) Avoid ax-mulf 11232. (Revised by GG, 16-Mar-2025.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴))) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐹 ∈ (IIHomeo(𝐽 ↾t (𝐴[,]𝐵)))) | ||
Theorem | icchmeoOLD 24985* | Obsolete version of icchmeo 24984 as of 9-Apr-2025. (Contributed by Mario Carneiro, 8-Sep-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐹 = (𝑥 ∈ (0[,]1) ↦ ((𝑥 · 𝐵) + ((1 − 𝑥) · 𝐴))) ⇒ ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵) → 𝐹 ∈ (IIHomeo(𝐽 ↾t (𝐴[,]𝐵)))) | ||
Theorem | icopnfcnv 24986* | 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 24987* | 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 24988* | 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 24989 | 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 24990* | 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 24991 | The extended reals are homeomorphic to the interval [0, 1]. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ II ≃ (ordTop‘ ≤ ) | ||
Theorem | xrcmp 24992 | The topology of the extended reals is compact. Since the topology of the extended reals extends the topology of the reals (by xrtgioo 24841), this means that ℝ* is a compactification of ℝ. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ (ordTop‘ ≤ ) ∈ Comp | ||
Theorem | xrconn 24993 | The topology of the extended reals is connected. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ (ordTop‘ ≤ ) ∈ Conn | ||
Theorem | icccvx 24994 | 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 24995* | 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 24996* | 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 24997* | The canonical bijection from (ℝ × ℝ) to ℂ described in cnref1o 13024 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.) Avoid ax-mulf 11232. (Revised by GG, 16-Mar-2025.) |
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐹 ∈ ((𝐽 ×t 𝐽)Homeo𝐾) | ||
Theorem | cnrehmeoOLD 24998* | Obsolete version of cnrehmeo 24997 as of 9-Apr-2025. (Contributed by Mario Carneiro, 25-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐹 ∈ ((𝐽 ×t 𝐽)Homeo𝐾) | ||
Theorem | cnheiborlem 24999* | Lemma for cnheibor 25000. (Contributed by Mario Carneiro, 14-Sep-2014.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝑇 = (𝐽 ↾t 𝑋) & ⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) & ⊢ 𝑌 = (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ⇒ ⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑇 ∈ Comp) | ||
Theorem | cnheibor 25000* | 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‘𝑥) ≤ 𝑟))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |