Home | Metamath
Proof Explorer Theorem List (p. 236 of 450) | < 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-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cncfrss 23501 | Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐴 ⊆ ℂ) | ||
Theorem | cncfrss2 23502 | Reverse closure of the continuous function predicate. (Contributed by Mario Carneiro, 25-Aug-2014.) |
⊢ (𝐹 ∈ (𝐴–cn→𝐵) → 𝐵 ⊆ ℂ) | ||
Theorem | cncff 23503 | 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 23504* | 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 23505* | Membership in the set of continuous complex functions from 𝐴 to 𝐵. (Contributed by Paul Chapman, 26-Nov-2007.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+) → 𝑍 ∈ ℝ+)) & ⊢ (𝜑 → (((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ ℝ+) → ((abs‘(𝑥 − 𝑤)) < 𝑍 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦))) ⇒ ⊢ (𝜑 → ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → 𝐹 ∈ (𝐴–cn→𝐵))) | ||
Theorem | elcncf1ii 23506* | Membership in the set of continuous complex functions from 𝐴 to 𝐵. (Contributed by Paul Chapman, 26-Nov-2007.) |
⊢ 𝐹:𝐴⟶𝐵 & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ℝ+) → 𝑍 ∈ ℝ+) & ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ 𝑦 ∈ ℝ+) → ((abs‘(𝑥 − 𝑤)) < 𝑍 → (abs‘((𝐹‘𝑥) − (𝐹‘𝑤))) < 𝑦)) ⇒ ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → 𝐹 ∈ (𝐴–cn→𝐵)) | ||
Theorem | rescncf 23507 | 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 23508 | 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 23509 | The set of continuous functions is expanded when the range is expanded. (Contributed by Mario Carneiro, 30-Aug-2014.) |
⊢ ((𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ℂ) → (𝐴–cn→𝐵) ⊆ (𝐴–cn→𝐶)) | ||
Theorem | climcncf 23510 | Image of a limit under a continuous map. (Contributed by Mario Carneiro, 7-Apr-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐹 ∈ (𝐴–cn→𝐵)) & ⊢ (𝜑 → 𝐺:𝑍⟶𝐴) & ⊢ (𝜑 → 𝐺 ⇝ 𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝐺) ⇝ (𝐹‘𝐷)) | ||
Theorem | abscncf 23511 | Absolute value is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
⊢ abs ∈ (ℂ–cn→ℝ) | ||
Theorem | recncf 23512 | Real part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
⊢ ℜ ∈ (ℂ–cn→ℝ) | ||
Theorem | imcncf 23513 | Imaginary part is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
⊢ ℑ ∈ (ℂ–cn→ℝ) | ||
Theorem | cjcncf 23514 | Complex conjugate is continuous. (Contributed by Paul Chapman, 21-Oct-2007.) (Revised by Mario Carneiro, 28-Apr-2014.) |
⊢ ∗ ∈ (ℂ–cn→ℂ) | ||
Theorem | mulc1cncf 23515* | Multiplication by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 30-Apr-2014.) |
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝐴 · 𝑥)) ⇒ ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ (ℂ–cn→ℂ)) | ||
Theorem | divccncf 23516* | Division by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) |
⊢ 𝐹 = (𝑥 ∈ ℂ ↦ (𝑥 / 𝐴)) ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → 𝐹 ∈ (ℂ–cn→ℂ)) | ||
Theorem | cncfco 23517 | 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 23518 | 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 23519 | Relate complex function continuity to topological continuity. (Contributed by Mario Carneiro, 17-Feb-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (𝐽 ↾t 𝐴) & ⊢ 𝐿 = (𝐽 ↾t 𝐵) ⇒ ⊢ ((𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ) → (𝐴–cn→𝐵) = (𝐾 Cn 𝐿)) | ||
Theorem | cncfcn1 23520 | 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 23521* | 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 23522* | 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 23523* | Composition of continuous functions. –cn→ analogue of cnmpt11f 22274. (Contributed by Mario Carneiro, 3-Sep-2014.) |
⊢ (𝜑 → 𝐹 ∈ (ℂ–cn→ℂ)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐹‘𝐴)) ∈ (𝑋–cn→ℂ)) | ||
Theorem | cncfmpt2f 23524* | Composition of continuous functions. –cn→ analogue of cnmpt12f 22276. (Contributed by Mario Carneiro, 3-Sep-2014.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ (𝜑 → 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴𝐹𝐵)) ∈ (𝑋–cn→ℂ)) | ||
Theorem | cncfmpt2ss 23525* | Composition of continuous functions in a subset. (Contributed by Mario Carneiro, 17-May-2016.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐹 ∈ ((𝐽 ×t 𝐽) Cn 𝐽) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→𝑆)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→𝑆)) & ⊢ 𝑆 ⊆ ℂ & ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴𝐹𝐵)) ∈ (𝑋–cn→𝑆)) | ||
Theorem | addccncf 23526* | 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 23527* | Division with a constant numerator is continuous. (Contributed by Mario Carneiro, 28-Dec-2016.) |
⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝐴 / 𝑥)) ⇒ ⊢ (𝐴 ∈ ℂ → 𝐹 ∈ ((ℂ ∖ {0})–cn→ℂ)) | ||
Theorem | negcncf 23528* | The negative function is continuous. (Contributed by Mario Carneiro, 30-Dec-2016.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ -𝑥) ⇒ ⊢ (𝐴 ⊆ ℂ → 𝐹 ∈ (𝐴–cn→ℂ)) | ||
Theorem | negfcncf 23529* | 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 23530 | Absolute value is continuous. Alternate proof of abscncf 23511. (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 23531 | Rewrite cmphaushmeo 22410 for functions on the complex numbers. (Contributed by Mario Carneiro, 19-Feb-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝐾 = (𝐽 ↾t 𝑋) ⇒ ⊢ ((𝐾 ∈ Comp ∧ 𝐹 ∈ (𝑋–cn→𝑌)) → (𝐹:𝑋–1-1-onto→𝑌 ↔ ◡𝐹 ∈ (𝑌–cn→𝑋))) | ||
Theorem | expcncf 23532* | The power function on complex numbers, for fixed exponent N, is continuous. Similar to expcn 23482. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
⊢ (𝑁 ∈ ℕ0 → (𝑥 ∈ ℂ ↦ (𝑥↑𝑁)) ∈ (ℂ–cn→ℂ)) | ||
Theorem | cnmptre 23533* | Lemma for iirevcn 23536 and related functions. (Contributed by Mario Carneiro, 6-Jun-2014.) |
⊢ 𝑅 = (TopOpen‘ℂfld) & ⊢ 𝐽 = ((topGen‘ran (,)) ↾t 𝐴) & ⊢ 𝐾 = ((topGen‘ran (,)) ↾t 𝐵) & ⊢ (𝜑 → 𝐴 ⊆ ℝ) & ⊢ (𝜑 → 𝐵 ⊆ ℝ) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → (𝑥 ∈ ℂ ↦ 𝐹) ∈ (𝑅 Cn 𝑅)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐹) ∈ (𝐽 Cn 𝐾)) | ||
Theorem | cnmpopc 23534* | 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 23535 | Reverse the unit interval. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑋 ∈ (0[,]1) → (1 − 𝑋) ∈ (0[,]1)) | ||
Theorem | iirevcn 23536 | 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 23537 | Map the first half of II into II. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑋 ∈ (0[,](1 / 2)) → (2 · 𝑋) ∈ (0[,]1)) | ||
Theorem | iihalf1cn 23538 | 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 23539 | Map the second half of II into II. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝑋 ∈ ((1 / 2)[,]1) → ((2 · 𝑋) − 1) ∈ (0[,]1)) | ||
Theorem | iihalf2cn 23540 | 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 23541 | Divide the unit interval into two pieces. (Contributed by Mario Carneiro, 7-Jun-2014.) |
⊢ (𝑋 ∈ (0[,](1 / 2)) ↔ (𝑋 ∈ (0[,]1) ∧ 𝑋 ≤ (1 / 2))) | ||
Theorem | elii2 23542 | Divide the unit interval into two pieces. (Contributed by Mario Carneiro, 7-Jun-2014.) |
⊢ ((𝑋 ∈ (0[,]1) ∧ ¬ 𝑋 ≤ (1 / 2)) → 𝑋 ∈ ((1 / 2)[,]1)) | ||
Theorem | iimulcl 23543 | The unit interval is closed under multiplication. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ((𝐴 ∈ (0[,]1) ∧ 𝐵 ∈ (0[,]1)) → (𝐴 · 𝐵) ∈ (0[,]1)) | ||
Theorem | iimulcn 23544* | 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 23545 | 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 23546 | 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 23547* | 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 23548* | 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 23549* | 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 23550* | 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 23551 | 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 23552* | 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 23553 | The extended reals are homeomorphic to the interval [0, 1]. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ II ≃ (ordTop‘ ≤ ) | ||
Theorem | xrcmp 23554 | The topology of the extended reals is compact. Since the topology of the extended reals extends the topology of the reals (by xrtgioo 23416), this means that ℝ* is a compactification of ℝ. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ (ordTop‘ ≤ ) ∈ Comp | ||
Theorem | xrconn 23555 | The topology of the extended reals is connected. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ (ordTop‘ ≤ ) ∈ Conn | ||
Theorem | icccvx 23556 | 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 23557* | 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 23558* | 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 23559* | The canonical bijection from (ℝ × ℝ) to ℂ described in cnref1o 12387 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 23560* | Lemma for cnheibor 23561. (Contributed by Mario Carneiro, 14-Sep-2014.) |
⊢ 𝐽 = (TopOpen‘ℂfld) & ⊢ 𝑇 = (𝐽 ↾t 𝑋) & ⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) & ⊢ 𝑌 = (𝐹 “ ((-𝑅[,]𝑅) × (-𝑅[,]𝑅))) ⇒ ⊢ ((𝑋 ∈ (Clsd‘𝐽) ∧ (𝑅 ∈ ℝ ∧ ∀𝑧 ∈ 𝑋 (abs‘𝑧) ≤ 𝑅)) → 𝑇 ∈ Comp) | ||
Theorem | cnheibor 23561* | 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 23562 | The topology on the complex numbers is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ 𝐽 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐽 ∈ 𝑛-Locally Comp | ||
Theorem | rellycmp 23563 | The topology on the reals is locally compact. (Contributed by Mario Carneiro, 2-Mar-2015.) |
⊢ (topGen‘ran (,)) ∈ 𝑛-Locally Comp | ||
Theorem | bndth 23564* | 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 23565* | 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 23566* | 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 23567* | Lemma for lebnum 23570. 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 23568* | Lemma for lebnum 23570. As a finite sum of point-to-set distance functions, which are continuous by metdscn 23466, 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 23569* | Lemma for lebnum 23570. 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 23570* | 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 23571* | Generalize lebnum 23570 to extended metrics. (Contributed by Mario Carneiro, 5-Sep-2015.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝐽 ∈ Comp) & ⊢ (𝜑 → 𝑈 ⊆ 𝐽) & ⊢ (𝜑 → 𝑋 = ∪ 𝑈) ⇒ ⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) | ||
Theorem | lebnumii 23572* | Specialize the Lebesgue number lemma lebnum 23570 to the closed unit interval. (Contributed by Mario Carneiro, 14-Feb-2015.) |
⊢ ((𝑈 ⊆ II ∧ (0[,]1) = ∪ 𝑈) → ∃𝑛 ∈ ℕ ∀𝑘 ∈ (1...𝑛)∃𝑢 ∈ 𝑈 (((𝑘 − 1) / 𝑛)[,](𝑘 / 𝑛)) ⊆ 𝑢) | ||
Syntax | chtpy 23573 | Extend class notation with the class of homotopies between two continuous functions. |
class Htpy | ||
Syntax | cphtpy 23574 | Extend class notation with the class of path homotopies between two continuous functions. |
class PHtpy | ||
Syntax | cphtpc 23575 | Extend class notation with the path homotopy relation. |
class ≃ph | ||
Definition | df-htpy 23576* | Define the function which takes topological spaces 𝑋, 𝑌 and two continuous functions 𝐹, 𝐺:𝑋⟶𝑌 and returns the class of homotopies from 𝐹 to 𝐺. (Contributed by Mario Carneiro, 22-Feb-2015.) |
⊢ Htpy = (𝑥 ∈ Top, 𝑦 ∈ Top ↦ (𝑓 ∈ (𝑥 Cn 𝑦), 𝑔 ∈ (𝑥 Cn 𝑦) ↦ {ℎ ∈ ((𝑥 ×t II) Cn 𝑦) ∣ ∀𝑠 ∈ ∪ 𝑥((𝑠ℎ0) = (𝑓‘𝑠) ∧ (𝑠ℎ1) = (𝑔‘𝑠))})) | ||
Definition | df-phtpy 23577* | Define the class of path homotopies between two paths 𝐹, 𝐺:II⟶𝑋; these are homotopies (in the sense of df-htpy 23576) which also preserve both endpoints of the paths throughout the homotopy. Definition of [Hatcher] p. 25. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ PHtpy = (𝑥 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑥), 𝑔 ∈ (II Cn 𝑥) ↦ {ℎ ∈ (𝑓(II Htpy 𝑥)𝑔) ∣ ∀𝑠 ∈ (0[,]1)((0ℎ𝑠) = (𝑓‘0) ∧ (1ℎ𝑠) = (𝑓‘1))})) | ||
Theorem | ishtpy 23578* | Membership in the class of homotopies between two continuous functions. (Contributed by Mario Carneiro, 22-Feb-2015.) (Revised by Mario Carneiro, 5-Sep-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → (𝐻 ∈ (𝐹(𝐽 Htpy 𝐾)𝐺) ↔ (𝐻 ∈ ((𝐽 ×t II) Cn 𝐾) ∧ ∀𝑠 ∈ 𝑋 ((𝑠𝐻0) = (𝐹‘𝑠) ∧ (𝑠𝐻1) = (𝐺‘𝑠))))) | ||
Theorem | htpycn 23579 | A homotopy is a continuous function. (Contributed by Mario Carneiro, 22-Feb-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → (𝐹(𝐽 Htpy 𝐾)𝐺) ⊆ ((𝐽 ×t II) Cn 𝐾)) | ||
Theorem | htpyi 23580 | A homotopy evaluated at its endpoints. (Contributed by Mario Carneiro, 22-Feb-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐻 ∈ (𝐹(𝐽 Htpy 𝐾)𝐺)) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑋) → ((𝐴𝐻0) = (𝐹‘𝐴) ∧ (𝐴𝐻1) = (𝐺‘𝐴))) | ||
Theorem | ishtpyd 23581* | Deduction for membership in the class of homotopies. (Contributed by Mario Carneiro, 22-Feb-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐻 ∈ ((𝐽 ×t II) Cn 𝐾)) & ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (𝑠𝐻0) = (𝐹‘𝑠)) & ⊢ ((𝜑 ∧ 𝑠 ∈ 𝑋) → (𝑠𝐻1) = (𝐺‘𝑠)) ⇒ ⊢ (𝜑 → 𝐻 ∈ (𝐹(𝐽 Htpy 𝐾)𝐺)) | ||
Theorem | htpycom 23582* | Given a homotopy from 𝐹 to 𝐺, produce a homotopy from 𝐺 to 𝐹. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾)) & ⊢ 𝑀 = (𝑥 ∈ 𝑋, 𝑦 ∈ (0[,]1) ↦ (𝑥𝐻(1 − 𝑦))) & ⊢ (𝜑 → 𝐻 ∈ (𝐹(𝐽 Htpy 𝐾)𝐺)) ⇒ ⊢ (𝜑 → 𝑀 ∈ (𝐺(𝐽 Htpy 𝐾)𝐹)) | ||
Theorem | htpyid 23583* | A homotopy from a function to itself. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ (0[,]1) ↦ (𝐹‘𝑥)) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝐹(𝐽 Htpy 𝐾)𝐹)) | ||
Theorem | htpyco1 23584* | Compose a homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ 𝑁 = (𝑥 ∈ 𝑋, 𝑦 ∈ (0[,]1) ↦ ((𝑃‘𝑥)𝐻𝑦)) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝑃 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐹 ∈ (𝐾 Cn 𝐿)) & ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐿)) & ⊢ (𝜑 → 𝐻 ∈ (𝐹(𝐾 Htpy 𝐿)𝐺)) ⇒ ⊢ (𝜑 → 𝑁 ∈ ((𝐹 ∘ 𝑃)(𝐽 Htpy 𝐿)(𝐺 ∘ 𝑃))) | ||
Theorem | htpyco2 23585 | Compose a homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝑃 ∈ (𝐾 Cn 𝐿)) & ⊢ (𝜑 → 𝐻 ∈ (𝐹(𝐽 Htpy 𝐾)𝐺)) ⇒ ⊢ (𝜑 → (𝑃 ∘ 𝐻) ∈ ((𝑃 ∘ 𝐹)(𝐽 Htpy 𝐿)(𝑃 ∘ 𝐺))) | ||
Theorem | htpycc 23586* | Concatenate two homotopies. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 23-Feb-2015.) |
⊢ 𝑁 = (𝑥 ∈ 𝑋, 𝑦 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 2), (𝑥𝐿(2 · 𝑦)), (𝑥𝑀((2 · 𝑦) − 1)))) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐻 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐿 ∈ (𝐹(𝐽 Htpy 𝐾)𝐺)) & ⊢ (𝜑 → 𝑀 ∈ (𝐺(𝐽 Htpy 𝐾)𝐻)) ⇒ ⊢ (𝜑 → 𝑁 ∈ (𝐹(𝐽 Htpy 𝐾)𝐻)) | ||
Theorem | isphtpy 23587* | Membership in the class of path homotopies between two continuous functions. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) ⇒ ⊢ (𝜑 → (𝐻 ∈ (𝐹(PHtpy‘𝐽)𝐺) ↔ (𝐻 ∈ (𝐹(II Htpy 𝐽)𝐺) ∧ ∀𝑠 ∈ (0[,]1)((0𝐻𝑠) = (𝐹‘0) ∧ (1𝐻𝑠) = (𝐹‘1))))) | ||
Theorem | phtpyhtpy 23588 | A path homotopy is a homotopy. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) ⇒ ⊢ (𝜑 → (𝐹(PHtpy‘𝐽)𝐺) ⊆ (𝐹(II Htpy 𝐽)𝐺)) | ||
Theorem | phtpycn 23589 | A path homotopy is a continuous function. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) ⇒ ⊢ (𝜑 → (𝐹(PHtpy‘𝐽)𝐺) ⊆ ((II ×t II) Cn 𝐽)) | ||
Theorem | phtpyi 23590 | Membership in the class of path homotopies between two continuous functions. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐻 ∈ (𝐹(PHtpy‘𝐽)𝐺)) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ (0[,]1)) → ((0𝐻𝐴) = (𝐹‘0) ∧ (1𝐻𝐴) = (𝐹‘1))) | ||
Theorem | phtpy01 23591 | Two path-homotopic paths have the same start and end point. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐻 ∈ (𝐹(PHtpy‘𝐽)𝐺)) ⇒ ⊢ (𝜑 → ((𝐹‘0) = (𝐺‘0) ∧ (𝐹‘1) = (𝐺‘1))) | ||
Theorem | isphtpyd 23592* | Deduction for membership in the class of path homotopies. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐻 ∈ (𝐹(II Htpy 𝐽)𝐺)) & ⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (0𝐻𝑠) = (𝐹‘0)) & ⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (1𝐻𝑠) = (𝐹‘1)) ⇒ ⊢ (𝜑 → 𝐻 ∈ (𝐹(PHtpy‘𝐽)𝐺)) | ||
Theorem | isphtpy2d 23593* | Deduction for membership in the class of path homotopies. (Contributed by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐻 ∈ ((II ×t II) Cn 𝐽)) & ⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝑠𝐻0) = (𝐹‘𝑠)) & ⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (𝑠𝐻1) = (𝐺‘𝑠)) & ⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (0𝐻𝑠) = (𝐹‘0)) & ⊢ ((𝜑 ∧ 𝑠 ∈ (0[,]1)) → (1𝐻𝑠) = (𝐹‘1)) ⇒ ⊢ (𝜑 → 𝐻 ∈ (𝐹(PHtpy‘𝐽)𝐺)) | ||
Theorem | phtpycom 23594* | Given a homotopy from 𝐹 to 𝐺, produce a homotopy from 𝐺 to 𝐹. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 23-Feb-2015.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) & ⊢ 𝐾 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝑥𝐻(1 − 𝑦))) & ⊢ (𝜑 → 𝐻 ∈ (𝐹(PHtpy‘𝐽)𝐺)) ⇒ ⊢ (𝜑 → 𝐾 ∈ (𝐺(PHtpy‘𝐽)𝐹)) | ||
Theorem | phtpyid 23595* | A homotopy from a path to itself. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 23-Feb-2015.) |
⊢ 𝐺 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ (𝐹‘𝑥)) & ⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝐹(PHtpy‘𝐽)𝐹)) | ||
Theorem | phtpyco2 23596 | Compose a path homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝑃 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐻 ∈ (𝐹(PHtpy‘𝐽)𝐺)) ⇒ ⊢ (𝜑 → (𝑃 ∘ 𝐻) ∈ ((𝑃 ∘ 𝐹)(PHtpy‘𝐾)(𝑃 ∘ 𝐺))) | ||
Theorem | phtpycc 23597* | Concatenate two path homotopies. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 7-Jun-2014.) |
⊢ 𝑀 = (𝑥 ∈ (0[,]1), 𝑦 ∈ (0[,]1) ↦ if(𝑦 ≤ (1 / 2), (𝑥𝐾(2 · 𝑦)), (𝑥𝐿((2 · 𝑦) − 1)))) & ⊢ (𝜑 → 𝐹 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐻 ∈ (II Cn 𝐽)) & ⊢ (𝜑 → 𝐾 ∈ (𝐹(PHtpy‘𝐽)𝐺)) & ⊢ (𝜑 → 𝐿 ∈ (𝐺(PHtpy‘𝐽)𝐻)) ⇒ ⊢ (𝜑 → 𝑀 ∈ (𝐹(PHtpy‘𝐽)𝐻)) | ||
Definition | df-phtpc 23598* | Define the function which takes a topology and returns the path homotopy relation on that topology. Definition of [Hatcher] p. 25. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Jun-2014.) |
⊢ ≃ph = (𝑥 ∈ Top ↦ {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ (II Cn 𝑥) ∧ (𝑓(PHtpy‘𝑥)𝑔) ≠ ∅)}) | ||
Theorem | phtpcrel 23599 | The path homotopy relation is a relation. (Contributed by Mario Carneiro, 7-Jun-2014.) (Revised by Mario Carneiro, 7-Aug-2014.) |
⊢ Rel ( ≃ph‘𝐽) | ||
Theorem | isphtpc 23600 | The relation "is path homotopic to". (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 5-Sep-2015.) |
⊢ (𝐹( ≃ph‘𝐽)𝐺 ↔ (𝐹 ∈ (II Cn 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽) ∧ (𝐹(PHtpy‘𝐽)𝐺) ≠ ∅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |