HomeTheorem List (p. 346 of 511)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 346 of 511) | < 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-31520) |
Hilbert Space Explorer
(31521-33043) |
Users' Mathboxes
(33044-51033) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | madjusmdetlem1 34501* | Lemma for madjusmdet 34505. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
| ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐷 = ((1...𝑁) maDet 𝑅) & ⊢ 𝐾 = ((1...𝑁) maAdju 𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) & ⊢ 𝐺 = (Base‘(SymGrp‘(1...𝑁))) & ⊢ 𝑆 = (pmSgn‘(1...𝑁)) & ⊢ 𝑈 = (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽) & ⊢ 𝑊 = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)𝑈(𝑄‘𝑗))) & ⊢ (𝜑 → 𝑃 ∈ 𝐺) & ⊢ (𝜑 → 𝑄 ∈ 𝐺) & ⊢ (𝜑 → (𝑃‘𝑁) = 𝐼) & ⊢ (𝜑 → (𝑄‘𝑁) = 𝐽) & ⊢ (𝜑 → (𝐼(subMat1‘𝑈)𝐽) = (𝑁(subMat1‘𝑊)𝑁)) ⇒ ⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽)))) | ||
| Theorem | madjusmdetlem2 34502* | Lemma for madjusmdet 34505. (Contributed by Thierry Arnoux, 26-Aug-2020.) |
| ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐷 = ((1...𝑁) maDet 𝑅) & ⊢ 𝐾 = ((1...𝑁) maAdju 𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) & ⊢ 𝑃 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) & ⊢ 𝑆 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝑁, if(𝑖 ≤ 𝑁, (𝑖 − 1), 𝑖))) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)) = ((𝑃 ∘ ◡𝑆)‘𝑋)) | ||
| Theorem | madjusmdetlem3 34503* | Lemma for madjusmdet 34505. (Contributed by Thierry Arnoux, 27-Aug-2020.) |
| ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐷 = ((1...𝑁) maDet 𝑅) & ⊢ 𝐾 = ((1...𝑁) maAdju 𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) & ⊢ 𝑃 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) & ⊢ 𝑆 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝑁, if(𝑖 ≤ 𝑁, (𝑖 − 1), 𝑖))) & ⊢ 𝑄 = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝐽, if(𝑗 ≤ 𝐽, (𝑗 − 1), 𝑗))) & ⊢ 𝑇 = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝑁, if(𝑗 ≤ 𝑁, (𝑗 − 1), 𝑗))) & ⊢ 𝑊 = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ (((𝑃 ∘ ◡𝑆)‘𝑖)𝑈((𝑄 ∘ ◡𝑇)‘𝑗))) & ⊢ (𝜑 → 𝑈 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼(subMat1‘𝑈)𝐽) = (𝑁(subMat1‘𝑊)𝑁)) | ||
| Theorem | madjusmdetlem4 34504* | Lemma for madjusmdet 34505. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
| ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐷 = ((1...𝑁) maDet 𝑅) & ⊢ 𝐾 = ((1...𝑁) maAdju 𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) & ⊢ 𝑃 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) & ⊢ 𝑆 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝑁, if(𝑖 ≤ 𝑁, (𝑖 − 1), 𝑖))) & ⊢ 𝑄 = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝐽, if(𝑗 ≤ 𝐽, (𝑗 − 1), 𝑗))) & ⊢ 𝑇 = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝑁, if(𝑗 ≤ 𝑁, (𝑗 − 1), 𝑗))) ⇒ ⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = ((𝑍‘( -1↑(𝐼 + 𝐽))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽)))) | ||
| Theorem | madjusmdet 34505 | Express the cofactor of the matrix, i.e. the entries of its adjunct matrix, using determinant of submatrices. (Contributed by Thierry Arnoux, 23-Aug-2020.) |
| ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐷 = ((1...𝑁) maDet 𝑅) & ⊢ 𝐾 = ((1...𝑁) maAdju 𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = ((𝑍‘( -1↑(𝐼 + 𝐽))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽)))) | ||
| Theorem | mdetlap 34506* | Laplace expansion of the determinant of a square matrix. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
| ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐷 = ((1...𝑁) maDet 𝑅) & ⊢ 𝐾 = ((1...𝑁) maAdju 𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐷‘𝑀) = (𝑅 Σg (𝑗 ∈ (1...𝑁) ↦ ((𝑍‘( -1↑(𝐼 + 𝑗))) · ((𝐼𝑀𝑗) · (𝐸‘(𝐼(subMat1‘𝑀)𝑗))))))) | ||
| Theorem | ist0cld 34507* | The predicate "is a T0 space", using closed sets. (Contributed by Thierry Arnoux, 16-Aug-2020.) |
| ⊢ (𝜑 → 𝐵 = ∪ 𝐽) & ⊢ (𝜑 → 𝐷 = (Clsd‘𝐽)) ⇒ ⊢ (𝜑 → (𝐽 ∈ Kol2 ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∀𝑑 ∈ 𝐷 (𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑) → 𝑥 = 𝑦)))) | ||
| Theorem | txomap 34508* | Given two open maps 𝐹 and 𝐺, 𝐻 mapping pairs of sets, is also an open map for the product topology. (Contributed by Thierry Arnoux, 29-Dec-2019.) |
| ⊢ (𝜑 → 𝐹:𝑋⟶𝑍) & ⊢ (𝜑 → 𝐺:𝑌⟶𝑇) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) & ⊢ (𝜑 → 𝑀 ∈ (TopOn‘𝑇)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ 𝐿) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐺 “ 𝑦) ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ (𝐽 ×t 𝐾)) & ⊢ 𝐻 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩) ⇒ ⊢ (𝜑 → (𝐻 “ 𝐴) ∈ (𝐿 ×t 𝑀)) | ||
| Theorem | qtopt1 34509* | If every equivalence class is closed, then the quotient space is T1 . (Contributed by Thierry Arnoux, 5-Jan-2020.) |
| ⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝐽 ∈ Fre) & ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (◡𝐹 “ {𝑥}) ∈ (Clsd‘𝐽)) ⇒ ⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ Fre) | ||
| Theorem | qtophaus 34510* | If an open map's graph in the product space (𝐽 ×t 𝐽) is closed, then its quotient topology is Hausdorff. (Contributed by Thierry Arnoux, 4-Jan-2020.) |
| ⊢ 𝑋 = ∪ 𝐽 & ⊢ ∼ = (◡𝐹 ∘ 𝐹) & ⊢ 𝐻 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) & ⊢ (𝜑 → 𝐽 ∈ Haus) & ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹)) & ⊢ (𝜑 → ∼ ∈ (Clsd‘(𝐽 ×t 𝐽))) ⇒ ⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ Haus) | ||
| Theorem | circtopn 34511* | The topology of the unit circle is generated by open intervals of the polar coordinate. (Contributed by Thierry Arnoux, 4-Jan-2020.) |
| ⊢ 𝐼 = (0[,](2 · π)) & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (exp‘(i · 𝑥))) & ⊢ 𝐶 = (◡abs “ {1}) ⇒ ⊢ (𝐽 qTop 𝐹) = (TopOpen‘(𝐹 “s ℝfld)) | ||
| Theorem | circcn 34512* | The function gluing the real line into the unit circle is continuous. (Contributed by Thierry Arnoux, 5-Jan-2020.) |
| ⊢ 𝐼 = (0[,](2 · π)) & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (exp‘(i · 𝑥))) & ⊢ 𝐶 = (◡abs “ {1}) ⇒ ⊢ 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)) | ||
| Theorem | reff 34513* | For any cover refinement, there exists a function associating with each set in the refinement a set in the original cover containing it. This is sometimes used as a definition of refinement. Note that this definition uses the axiom of choice through ac6sg 10566. (Contributed by Thierry Arnoux, 12-Jan-2020.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴Ref𝐵 ↔ (∪ 𝐵 ⊆ ∪ 𝐴 ∧ ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑣 ∈ 𝐴 𝑣 ⊆ (𝑓‘𝑣))))) | ||
| Theorem | locfinreflem 34514* | A locally finite refinement of an open cover induces a locally finite open cover with the original index set. This is fact 2 of http://at.yorku.ca/p/a/c/a/02.pdf, it is expressed by exposing a function 𝑓 from the original cover 𝑈, which is taken as the index set. The solution is constructed by building unions, so the same method can be used to prove a similar theorem about closed covers. (Contributed by Thierry Arnoux, 29-Jan-2020.) |
| ⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝑈 ⊆ 𝐽) & ⊢ (𝜑 → 𝑋 = ∪ 𝑈) & ⊢ (𝜑 → 𝑉 ⊆ 𝐽) & ⊢ (𝜑 → 𝑉Ref𝑈) & ⊢ (𝜑 → 𝑉 ∈ (LocFin‘𝐽)) ⇒ ⊢ (𝜑 → ∃𝑓((Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))) | ||
| Theorem | locfinref 34515* | A locally finite refinement of an open cover induces a locally finite open cover with the original index set. This is fact 2 of http://at.yorku.ca/p/a/c/a/02.pdf, it is expressed by exposing a function 𝑓 from the original cover 𝑈, which is taken as the index set. (Contributed by Thierry Arnoux, 31-Jan-2020.) |
| ⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝑈 ⊆ 𝐽) & ⊢ (𝜑 → 𝑋 = ∪ 𝑈) & ⊢ (𝜑 → 𝑉 ⊆ 𝐽) & ⊢ (𝜑 → 𝑉Ref𝑈) & ⊢ (𝜑 → 𝑉 ∈ (LocFin‘𝐽)) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝑈⟶𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))) | ||
| Syntax | ccref 34516 | The "every open cover has an 𝐴 refinement" predicate. |
| class CovHasRef𝐴 | ||
| Definition | df-cref 34517* | Define a statement "every open cover has an 𝐴 refinement" , where 𝐴 is a property for refinements like "finite", "countable", "point finite" or "locally finite". (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ CovHasRef𝐴 = {𝑗 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑗(∪ 𝑗 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑗 ∩ 𝐴)𝑧Ref𝑦)} | ||
| Theorem | iscref 34518* | The property that every open cover has an 𝐴 refinement for the topological space 𝐽. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ CovHasRef𝐴 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝐽 ∩ 𝐴)𝑧Ref𝑦))) | ||
| Theorem | crefeq 34519 | Equality theorem for the "every open cover has an A refinement" predicate. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ (𝐴 = 𝐵 → CovHasRef𝐴 = CovHasRef𝐵) | ||
| Theorem | creftop 34520 | A space where every open cover has an 𝐴 refinement is a topological space. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ (𝐽 ∈ CovHasRef𝐴 → 𝐽 ∈ Top) | ||
| Theorem | crefi 34521* | The property that every open cover has an 𝐴 refinement for the topological space 𝐽. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ CovHasRef𝐴 ∧ 𝐶 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝐶) → ∃𝑧 ∈ (𝒫 𝐽 ∩ 𝐴)𝑧Ref𝐶) | ||
| Theorem | crefdf 34522* | A formulation of crefi 34521 easier to use for definitions. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐵 = CovHasRef𝐴 & ⊢ (𝑧 ∈ 𝐴 → 𝜑) ⇒ ⊢ ((𝐽 ∈ 𝐵 ∧ 𝐶 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝐶) → ∃𝑧 ∈ 𝒫 𝐽(𝜑 ∧ 𝑧Ref𝐶)) | ||
| Theorem | crefss 34523 | The "every open cover has an 𝐴 refinement" predicate respects inclusion. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ (𝐴 ⊆ 𝐵 → CovHasRef𝐴 ⊆ CovHasRef𝐵) | ||
| Theorem | cmpcref 34524 | Equivalent definition of compact space in terms of open cover refinements. Compact spaces are topologies with finite open cover refinements. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ Comp = CovHasRefFin | ||
| Theorem | cmpfiref 34525* | Every open cover of a Compact space has a finite refinement. (Contributed by Thierry Arnoux, 1-Feb-2020.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Comp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈) → ∃𝑣 ∈ 𝒫 𝐽(𝑣 ∈ Fin ∧ 𝑣Ref𝑈)) | ||
| Syntax | cldlf 34526 | Extend class notation with the class of all Lindelöf spaces. |
| class Ldlf | ||
| Definition | df-ldlf 34527 | Definition of a Lindelöf space. A Lindelöf space is a topological space in which every open cover has a countable subcover. Definition 1 of [BourbakiTop2] p. 195. (Contributed by Thierry Arnoux, 30-Jan-2020.) |
| ⊢ Ldlf = CovHasRef{𝑥 ∣ 𝑥 ≼ ω} | ||
| Theorem | ldlfcntref 34528* | Every open cover of a Lindelöf space has a countable refinement. (Contributed by Thierry Arnoux, 1-Feb-2020.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Ldlf ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈) → ∃𝑣 ∈ 𝒫 𝐽(𝑣 ≼ ω ∧ 𝑣Ref𝑈)) | ||
| Syntax | cpcmp 34529 | Extend class notation with the class of all paracompact topologies. |
| class Paracomp | ||
| Definition | df-pcmp 34530 | Definition of a paracompact topology. A topology is said to be paracompact iff every open cover has an open refinement that is locally finite. The definition 6 of [BourbakiTop1] p. I.69. also requires the topology to be Hausdorff, but this is dropped here. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ Paracomp = {𝑗 ∣ 𝑗 ∈ CovHasRef(LocFin‘𝑗)} | ||
| Theorem | ispcmp 34531 | The predicate "is a paracompact topology". (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ (𝐽 ∈ Paracomp ↔ 𝐽 ∈ CovHasRef(LocFin‘𝐽)) | ||
| Theorem | cmppcmp 34532 | Every compact space is paracompact. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ (𝐽 ∈ Comp → 𝐽 ∈ Paracomp) | ||
| Theorem | dispcmp 34533 | Every discrete space is paracompact. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ Paracomp) | ||
| Theorem | pcmplfin 34534* | Given a paracompact topology 𝐽 and an open cover 𝑈, there exists an open refinement 𝑣 that is locally finite. (Contributed by Thierry Arnoux, 31-Jan-2020.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Paracomp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈) → ∃𝑣 ∈ 𝒫 𝐽(𝑣 ∈ (LocFin‘𝐽) ∧ 𝑣Ref𝑈)) | ||
| Theorem | pcmplfinf 34535* | Given a paracompact topology 𝐽 and an open cover 𝑈, there exists an open refinement ran 𝑓 that is locally finite, using the same index as the original cover 𝑈. (Contributed by Thierry Arnoux, 31-Jan-2020.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Paracomp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈) → ∃𝑓(𝑓:𝑈⟶𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))) | ||
The prime ideals of a ring 𝑅 can be endowed with the Zariski topology. This is done by defining a function 𝑉 which maps ideals of 𝑅 to closed sets (see for example zarcls0 34542 for the definition of 𝑉). The closed sets of the topology are in the range of 𝑉 (see zartopon 34551). The correspondence with the open sets is made in zarcls 34548. As proved in zart0 34553, the Zariski topology is T0 , but generally not T1 . | ||
| Syntax | crspec 34536 | Extend class notation with the spectrum of a ring. |
| class Spec | ||
| Definition | df-rspec 34537 | Define the spectrum of a ring. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| ⊢ Spec = (𝑟 ∈ Ring ↦ ((IDLsrg‘𝑟) ↾s (PrmIdeal‘𝑟))) | ||
| Theorem | rspecval 34538 | Value of the spectrum of the ring 𝑅. Notation 1.1.1 of [EGA] p. 80. (Contributed by Thierry Arnoux, 2-Jun-2024.) |
| ⊢ (𝑅 ∈ Ring → (Spec‘𝑅) = ((IDLsrg‘𝑅) ↾s (PrmIdeal‘𝑅))) | ||
| Theorem | rspecbas 34539 | The prime ideals form the base of the spectrum of a ring. (Contributed by Thierry Arnoux, 2-Jun-2024.) |
| ⊢ 𝑆 = (Spec‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (PrmIdeal‘𝑅) = (Base‘𝑆)) | ||
| Theorem | rspectset 34540* | Topology component of the spectrum of a ring. (Contributed by Thierry Arnoux, 2-Jun-2024.) |
| ⊢ 𝑆 = (Spec‘𝑅) & ⊢ 𝐼 = (LIdeal‘𝑅) & ⊢ 𝐽 = ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) ⇒ ⊢ (𝑅 ∈ Ring → 𝐽 = (TopSet‘𝑆)) | ||
| Theorem | rspectopn 34541* | The topology component of the spectrum of a ring. (Contributed by Thierry Arnoux, 4-Jun-2024.) |
| ⊢ 𝑆 = (Spec‘𝑅) & ⊢ 𝐼 = (LIdeal‘𝑅) & ⊢ 𝑃 = (PrmIdeal‘𝑅) & ⊢ 𝐽 = ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗}) ⇒ ⊢ (𝑅 ∈ Ring → 𝐽 = (TopOpen‘𝑆)) | ||
| Theorem | zarcls0 34542* | The closure of the identity ideal in the Zariski topology. Proposition 1.1.2(i) of [EGA] p. 80. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
| ⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) & ⊢ 𝑃 = (PrmIdeal‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝑉‘{ 0 }) = 𝑃) | ||
| Theorem | zarcls1 34543* | The unit ideal 𝐵 is the only ideal whose closure in the Zariski topology is the empty set. Stronger form of the Proposition 1.1.2(i) of [EGA] p. 80. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
| ⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → ((𝑉‘𝐼) = ∅ ↔ 𝐼 = 𝐵)) | ||
| Theorem | zarclsun 34544* | The union of two closed sets of the Zariski topology is closed. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
| ⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ ran 𝑉 ∧ 𝑌 ∈ ran 𝑉) → (𝑋 ∪ 𝑌) ∈ ran 𝑉) | ||
| Theorem | zarclsiin 34545* | In a Zariski topology, the intersection of the closures of a family of ideals is the closure of the span of their union. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
| ⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) & ⊢ 𝐾 = (RSpan‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑇 ⊆ (LIdeal‘𝑅) ∧ 𝑇 ≠ ∅) → ∩ 𝑙 ∈ 𝑇 (𝑉‘𝑙) = (𝑉‘(𝐾‘∪ 𝑇))) | ||
| Theorem | zarclsint 34546* | The intersection of a family of closed sets is closed in the Zariski topology. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
| ⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ∧ 𝑆 ≠ ∅) → ∩ 𝑆 ∈ ran 𝑉) | ||
| Theorem | zarclssn 34547* | The closed points of Zariski topology are the maximal ideals. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
| ⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) & ⊢ 𝐵 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ({𝑀} = (𝑉‘𝑀) ↔ 𝑀 ∈ (MaxIdeal‘𝑅))) | ||
| Theorem | zarcls 34548* | The open sets of the Zariski topology are the complements of the closed sets. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
| ⊢ 𝑆 = (Spec‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑆) & ⊢ 𝑃 = (PrmIdeal‘𝑅) & ⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗}) ⇒ ⊢ (𝑅 ∈ Ring → 𝐽 = {𝑠 ∈ 𝒫 𝑃 ∣ (𝑃 ∖ 𝑠) ∈ ran 𝑉}) | ||
| Theorem | zartopn 34549* | The Zariski topology is a topology, and its closed sets are images by 𝑉 of the ideals of 𝑅. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
| ⊢ 𝑆 = (Spec‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑆) & ⊢ 𝑃 = (PrmIdeal‘𝑅) & ⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ 𝑃 ∣ 𝑖 ⊆ 𝑗}) ⇒ ⊢ (𝑅 ∈ CRing → (𝐽 ∈ (TopOn‘𝑃) ∧ ran 𝑉 = (Clsd‘𝐽))) | ||
| Theorem | zartop 34550 | The Zariski topology is a topology. Proposition 1.1.2 of [EGA] p. 80. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
| ⊢ 𝑆 = (Spec‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑆) ⇒ ⊢ (𝑅 ∈ CRing → 𝐽 ∈ Top) | ||
| Theorem | zartopon 34551 | The points of the Zariski topology are the prime ideals. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
| ⊢ 𝑆 = (Spec‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑆) & ⊢ 𝑃 = (PrmIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → 𝐽 ∈ (TopOn‘𝑃)) | ||
| Theorem | zar0ring 34552 | The Zariski Topology of the trivial ring. (Contributed by Thierry Arnoux, 1-Jul-2024.) |
| ⊢ 𝑆 = (Spec‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑆) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (♯‘𝐵) = 1) → 𝐽 = {∅}) | ||
| Theorem | zart0 34553 | The Zariski topology is T0 . Corollary 1.1.8 of [EGA] p. 81. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
| ⊢ 𝑆 = (Spec‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑆) ⇒ ⊢ (𝑅 ∈ CRing → 𝐽 ∈ Kol2) | ||
| Theorem | zarmxt1 34554 | The Zariski topology restricted to maximal ideals is T1 . (Contributed by Thierry Arnoux, 16-Jun-2024.) |
| ⊢ 𝑆 = (Spec‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑆) & ⊢ 𝑀 = (MaxIdeal‘𝑅) & ⊢ 𝑇 = (𝐽 ↾t 𝑀) ⇒ ⊢ (𝑅 ∈ CRing → 𝑇 ∈ Fre) | ||
| Theorem | zarcmplem 34555* | Lemma for zarcmp 34556. (Contributed by Thierry Arnoux, 2-Jul-2024.) |
| ⊢ 𝑆 = (Spec‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑆) & ⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) ⇒ ⊢ (𝑅 ∈ CRing → 𝐽 ∈ Comp) | ||
| Theorem | zarcmp 34556 | The Zariski topology is compact. Proposition 1.1.10(ii) of [EGA], p. 82. (Contributed by Thierry Arnoux, 2-Jul-2024.) |
| ⊢ 𝑆 = (Spec‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑆) ⇒ ⊢ (𝑅 ∈ CRing → 𝐽 ∈ Comp) | ||
| Theorem | rspectps 34557 | The spectrum of a ring 𝑅 is a topological space. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
| ⊢ 𝑆 = (Spec‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → 𝑆 ∈ TopSp) | ||
| Theorem | rhmpreimacnlem 34558* | Lemma for rhmpreimacn 34559. (Contributed by Thierry Arnoux, 7-Jul-2024.) |
| ⊢ 𝑇 = (Spec‘𝑅) & ⊢ 𝑈 = (Spec‘𝑆) & ⊢ 𝐴 = (PrmIdeal‘𝑅) & ⊢ 𝐵 = (PrmIdeal‘𝑆) & ⊢ 𝐽 = (TopOpen‘𝑇) & ⊢ 𝐾 = (TopOpen‘𝑈) & ⊢ 𝐺 = (𝑖 ∈ 𝐵 ↦ (◡𝐹 “ 𝑖)) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) & ⊢ (𝜑 → ran 𝐹 = (Base‘𝑆)) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ 𝑉 = (𝑗 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑗 ⊆ 𝑘}) & ⊢ 𝑊 = (𝑗 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑗 ⊆ 𝑘}) ⇒ ⊢ (𝜑 → (𝑊‘(𝐹 “ 𝐼)) = (◡𝐺 “ (𝑉‘𝐼))) | ||
| Theorem | rhmpreimacn 34559* | The function mapping a prime ideal to its preimage by a surjective ring homomorphism is continuous, when considering the Zariski topology. Corollary 1.2.3 of [EGA], p. 83. Notice that the direction of the continuous map 𝐺 is reverse: the original ring homomorphism 𝐹 goes from 𝑅 to 𝑆, but the continuous map 𝐺 goes from 𝐵 to 𝐴. This mapping is also called "induced map on prime spectra" or "pullback on primes". (Contributed by Thierry Arnoux, 8-Jul-2024.) |
| ⊢ 𝑇 = (Spec‘𝑅) & ⊢ 𝑈 = (Spec‘𝑆) & ⊢ 𝐴 = (PrmIdeal‘𝑅) & ⊢ 𝐵 = (PrmIdeal‘𝑆) & ⊢ 𝐽 = (TopOpen‘𝑇) & ⊢ 𝐾 = (TopOpen‘𝑈) & ⊢ 𝐺 = (𝑖 ∈ 𝐵 ↦ (◡𝐹 “ 𝑖)) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) & ⊢ (𝜑 → ran 𝐹 = (Base‘𝑆)) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽)) | ||
| Syntax | cmetid 34560 | Extend class notation with the class of metric identifications. |
| class ~Met | ||
| Syntax | cpstm 34561 | Extend class notation with the metric induced by a pseudometric. |
| class pstoMet | ||
| Definition | df-metid 34562* | Define the metric identification relation for a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| ⊢ ~Met = (𝑑 ∈ ∪ ran PsMet ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ dom dom 𝑑 ∧ 𝑦 ∈ dom dom 𝑑) ∧ (𝑥𝑑𝑦) = 0)}) | ||
| Definition | df-pstm 34563* | Define the metric induced by a pseudometric. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| ⊢ pstoMet = (𝑑 ∈ ∪ ran PsMet ↦ (𝑎 ∈ (dom dom 𝑑 / (~Met‘𝑑)), 𝑏 ∈ (dom dom 𝑑 / (~Met‘𝑑)) ↦ ∪ {𝑧 ∣ ∃𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝑧 = (𝑥𝑑𝑦)})) | ||
| Theorem | metidval 34564* | Value of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| ⊢ (𝐷 ∈ (PsMet‘𝑋) → (~Met‘𝐷) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑥𝐷𝑦) = 0)}) | ||
| Theorem | metidss 34565 | As a relation, the metric identification is a subset of a Cartesian product. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| ⊢ (𝐷 ∈ (PsMet‘𝑋) → (~Met‘𝐷) ⊆ (𝑋 × 𝑋)) | ||
| Theorem | metidv 34566 | 𝐴 and 𝐵 identify by the metric 𝐷 if their distance is zero. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴(~Met‘𝐷)𝐵 ↔ (𝐴𝐷𝐵) = 0)) | ||
| Theorem | metideq 34567 | Basic property of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐴𝐷𝐸) = (𝐵𝐷𝐹)) | ||
| Theorem | metider 34568 | The metric identification is an equivalence relation. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
| ⊢ (𝐷 ∈ (PsMet‘𝑋) → (~Met‘𝐷) Er 𝑋) | ||
| Theorem | pstmval 34569* | Value of the metric induced by a pseudometric 𝐷. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| ⊢ ∼ = (~Met‘𝐷) ⇒ ⊢ (𝐷 ∈ (PsMet‘𝑋) → (pstoMet‘𝐷) = (𝑎 ∈ (𝑋 / ∼ ), 𝑏 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧 ∣ ∃𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝑧 = (𝑥𝐷𝑦)})) | ||
| Theorem | pstmfval 34570 | Function value of the metric induced by a pseudometric 𝐷 (Contributed by Thierry Arnoux, 11-Feb-2018.) |
| ⊢ ∼ = (~Met‘𝐷) ⇒ ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ([𝐴] ∼ (pstoMet‘𝐷)[𝐵] ∼ ) = (𝐴𝐷𝐵)) | ||
| Theorem | pstmxmet 34571 | The metric induced by a pseudometric is a full-fledged metric on the equivalence classes of the metric identification. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
| ⊢ ∼ = (~Met‘𝐷) ⇒ ⊢ (𝐷 ∈ (PsMet‘𝑋) → (pstoMet‘𝐷) ∈ (∞Met‘(𝑋 / ∼ ))) | ||
| Theorem | hauseqcn 34572 | In a Hausdorff topology, two continuous functions which agree on a dense set agree everywhere. (Contributed by Thierry Arnoux, 28-Dec-2017.) |
| ⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝐾 ∈ Haus) & ⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾)) & ⊢ (𝜑 → (𝐹 ↾ 𝐴) = (𝐺 ↾ 𝐴)) & ⊢ (𝜑 → 𝐴 ⊆ 𝑋) & ⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝑋) ⇒ ⊢ (𝜑 → 𝐹 = 𝐺) | ||
| Theorem | elunitge0 34573 | An element of the closed unit interval is positive. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 20-Dec-2016.) |
| ⊢ (𝐴 ∈ (0[,]1) → 0 ≤ 𝐴) | ||
| Theorem | unitssxrge0 34574 | The closed unit interval is a subset of the set of the extended nonnegative reals. Useful lemma for manipulating probabilities within the closed unit interval. (Contributed by Thierry Arnoux, 12-Dec-2016.) |
| ⊢ (0[,]1) ⊆ (0[,]+∞) | ||
| Theorem | unitdivcld 34575 | Necessary conditions for a quotient to be in the closed unit interval. (somewhat too strong, it would be sufficient that A and B are in RR+) (Contributed by Thierry Arnoux, 20-Dec-2016.) |
| ⊢ ((𝐴 ∈ (0[,]1) ∧ 𝐵 ∈ (0[,]1) ∧ 𝐵 ≠ 0) → (𝐴 ≤ 𝐵 ↔ (𝐴 / 𝐵) ∈ (0[,]1))) | ||
| Theorem | iistmd 34576 | The closed unit interval forms a topological monoid under multiplication. (Contributed by Thierry Arnoux, 25-Mar-2017.) |
| ⊢ 𝐼 = ((mulGrp‘ℂfld) ↾s (0[,]1)) ⇒ ⊢ 𝐼 ∈ TopMnd | ||
| Theorem | unicls 34577 | The union of the closed set is the underlying set of the topology. (Contributed by Thierry Arnoux, 21-Sep-2017.) |
| ⊢ 𝐽 ∈ Top & ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ∪ (Clsd‘𝐽) = 𝑋 | ||
| Theorem | tpr2tp 34578 | The usual topology on (ℝ × ℝ) is the product topology of the usual topology on ℝ. (Contributed by Thierry Arnoux, 21-Sep-2017.) |
| ⊢ 𝐽 = (topGen‘ran (,)) ⇒ ⊢ (𝐽 ×t 𝐽) ∈ (TopOn‘(ℝ × ℝ)) | ||
| Theorem | tpr2uni 34579 | The usual topology on (ℝ × ℝ) is the product topology of the usual topology on ℝ. (Contributed by Thierry Arnoux, 21-Sep-2017.) |
| ⊢ 𝐽 = (topGen‘ran (,)) ⇒ ⊢ ∪ (𝐽 ×t 𝐽) = (ℝ × ℝ) | ||
| Theorem | xpinpreima 34580 | Rewrite the cartesian product of two sets as the intersection of their preimage by 1st and 2nd, the projections on the first and second elements. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
| ⊢ (𝐴 × 𝐵) = ((◡(1st ↾ (V × V)) “ 𝐴) ∩ (◡(2nd ↾ (V × V)) “ 𝐵)) | ||
| Theorem | xpinpreima2 34581 | Rewrite the cartesian product of two sets as the intersection of their preimage by 1st and 2nd, the projections on the first and second elements. (Contributed by Thierry Arnoux, 22-Sep-2017.) |
| ⊢ ((𝐴 ⊆ 𝐸 ∧ 𝐵 ⊆ 𝐹) → (𝐴 × 𝐵) = ((◡(1st ↾ (𝐸 × 𝐹)) “ 𝐴) ∩ (◡(2nd ↾ (𝐸 × 𝐹)) “ 𝐵))) | ||
| Theorem | sqsscirc1 34582 | The complex square of side 𝐷 is a subset of the complex circle of radius 𝐷. (Contributed by Thierry Arnoux, 25-Sep-2017.) |
| ⊢ ((((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) ∧ (𝑌 ∈ ℝ ∧ 0 ≤ 𝑌)) ∧ 𝐷 ∈ ℝ+) → ((𝑋 < (𝐷 / 2) ∧ 𝑌 < (𝐷 / 2)) → (√‘((𝑋↑2) + (𝑌↑2))) < 𝐷)) | ||
| Theorem | sqsscirc2 34583 | The complex square of side 𝐷 is a subset of the complex disc of radius 𝐷. (Contributed by Thierry Arnoux, 25-Sep-2017.) |
| ⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) ∧ 𝐷 ∈ ℝ+) → (((abs‘(ℜ‘(𝐵 − 𝐴))) < (𝐷 / 2) ∧ (abs‘(ℑ‘(𝐵 − 𝐴))) < (𝐷 / 2)) → (abs‘(𝐵 − 𝐴)) < 𝐷)) | ||
| Theorem | cnre2csqlem 34584* | Lemma for cnre2csqima 34585. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
| ⊢ (𝐺 ↾ (ℝ × ℝ)) = (𝐻 ∘ 𝐹) & ⊢ 𝐹 Fn (ℝ × ℝ) & ⊢ 𝐺 Fn V & ⊢ (𝑥 ∈ (ℝ × ℝ) → (𝐺‘𝑥) ∈ ℝ) & ⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → (𝐻‘(𝑥 − 𝑦)) = ((𝐻‘𝑥) − (𝐻‘𝑦))) ⇒ ⊢ ((𝑋 ∈ (ℝ × ℝ) ∧ 𝑌 ∈ (ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝑌 ∈ (◡(𝐺 ↾ (ℝ × ℝ)) “ (((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷))) → (abs‘(𝐻‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷)) | ||
| Theorem | cnre2csqima 34585* | Image of a centered square by the canonical bijection from (ℝ × ℝ) to ℂ. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
| ⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦))) ⇒ ⊢ ((𝑋 ∈ (ℝ × ℝ) ∧ 𝑌 ∈ (ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝑌 ∈ ((((1st ‘𝑋) − 𝐷)(,)((1st ‘𝑋) + 𝐷)) × (((2nd ‘𝑋) − 𝐷)(,)((2nd ‘𝑋) + 𝐷))) → ((abs‘(ℜ‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷 ∧ (abs‘(ℑ‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷))) | ||
| Theorem | tpr2rico 34586* | For any point of an open set of the usual topology on (ℝ × ℝ) there is an open square which contains that point and is entirely in the open set. This is square is actually a ball by the (𝑙↑+∞) norm 𝑋. (Contributed by Thierry Arnoux, 21-Sep-2017.) |
| ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐺 = (𝑢 ∈ ℝ, 𝑣 ∈ ℝ ↦ (𝑢 + (i · 𝑣))) & ⊢ 𝐵 = ran (𝑥 ∈ ran (,), 𝑦 ∈ ran (,) ↦ (𝑥 × 𝑦)) ⇒ ⊢ ((𝐴 ∈ (𝐽 ×t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∃𝑟 ∈ 𝐵 (𝑋 ∈ 𝑟 ∧ 𝑟 ⊆ 𝐴)) | ||
| Theorem | cnvordtrestixx 34587* | The restriction of the 'greater than' order to an interval gives the same topology as the subspace topology. (Contributed by Thierry Arnoux, 1-Apr-2017.) |
| ⊢ 𝐴 ⊆ ℝ* & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥[,]𝑦) ⊆ 𝐴) ⇒ ⊢ ((ordTop‘ ≤ ) ↾t 𝐴) = (ordTop‘(◡ ≤ ∩ (𝐴 × 𝐴))) | ||
| Theorem | prsdm 34588 | Domain of the relation of a proset. (Contributed by Thierry Arnoux, 11-Sep-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ (𝐾 ∈ Proset → dom ≤ = 𝐵) | ||
| Theorem | prsrn 34589 | Range of the relation of a proset. (Contributed by Thierry Arnoux, 11-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ (𝐾 ∈ Proset → ran ≤ = 𝐵) | ||
| Theorem | prsss 34590 | Relation of a subproset. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → ( ≤ ∩ (𝐴 × 𝐴)) = ((le‘𝐾) ∩ (𝐴 × 𝐴))) | ||
| Theorem | prsssdm 34591 | Domain of a subproset relation. (Contributed by Thierry Arnoux, 12-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → dom ( ≤ ∩ (𝐴 × 𝐴)) = 𝐴) | ||
| Theorem | ordtprsval 34592* | Value of the order topology for a proset. (Contributed by Thierry Arnoux, 11-Sep-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ 𝐸 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) & ⊢ 𝐹 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ⇒ ⊢ (𝐾 ∈ Proset → (ordTop‘ ≤ ) = (topGen‘(fi‘({𝐵} ∪ (𝐸 ∪ 𝐹))))) | ||
| Theorem | ordtprsuni 34593* | Value of the order topology. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ 𝐸 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) & ⊢ 𝐹 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ⇒ ⊢ (𝐾 ∈ Proset → 𝐵 = ∪ ({𝐵} ∪ (𝐸 ∪ 𝐹))) | ||
| Theorem | ordtcnvNEW 34594 | The order dual generates the same topology as the original order. (Contributed by Mario Carneiro, 3-Sep-2015.) (Revised by Thierry Arnoux, 13-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ (𝐾 ∈ Proset → (ordTop‘◡ ≤ ) = (ordTop‘ ≤ )) | ||
| Theorem | ordtrestNEW 34595 | The subspace topology of an order topology is in general finer than the topology generated by the restricted order, but we do have inclusion in one direction. (Contributed by Mario Carneiro, 9-Sep-2015.) (Revised by Thierry Arnoux, 11-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) ⊆ ((ordTop‘ ≤ ) ↾t 𝐴)) | ||
| Theorem | ordtrest2NEWlem 34596* | Lemma for ordtrest2NEW 34597. (Contributed by Mario Carneiro, 9-Sep-2015.) (Revised by Thierry Arnoux, 11-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ (𝜑 → 𝐾 ∈ Toset) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝐵 ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} ⊆ 𝐴) ⇒ ⊢ (𝜑 → ∀𝑣 ∈ ran (𝑧 ∈ 𝐵 ↦ {𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧})(𝑣 ∩ 𝐴) ∈ (ordTop‘( ≤ ∩ (𝐴 × 𝐴)))) | ||
| Theorem | ordtrest2NEW 34597* | An interval-closed set 𝐴 in a total order has the same subspace topology as the restricted order topology. (An interval-closed set is the same thing as an open or half-open or closed interval in ℝ, but in other sets like ℚ there are interval-closed sets like (π, +∞) ∩ ℚ that are not intervals.) (Contributed by Mario Carneiro, 9-Sep-2015.) (Revised by Thierry Arnoux, 11-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ (𝜑 → 𝐾 ∈ Toset) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → {𝑧 ∈ 𝐵 ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)} ⊆ 𝐴) ⇒ ⊢ (𝜑 → (ordTop‘( ≤ ∩ (𝐴 × 𝐴))) = ((ordTop‘ ≤ ) ↾t 𝐴)) | ||
| Theorem | ordtconnlem1 34598* | Connectedness in the order topology of a toset. This is the "easy" direction of ordtconn 34599. See also reconnlem1 25146. (Contributed by Thierry Arnoux, 14-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ 𝐽 = (ordTop‘ ≤ ) ⇒ ⊢ ((𝐾 ∈ Toset ∧ 𝐴 ⊆ 𝐵) → ((𝐽 ↾t 𝐴) ∈ Conn → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑟 ∈ 𝐵 ((𝑥 ≤ 𝑟 ∧ 𝑟 ≤ 𝑦) → 𝑟 ∈ 𝐴))) | ||
| Theorem | ordtconn 34599 | Connectedness in the order topology of a complete uniform totally ordered space. (Contributed by Thierry Arnoux, 15-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ 𝐽 = (ordTop‘ ≤ ) ⇒ ⊢ ⊤ | ||
| Theorem | mndpluscn 34600* | A mapping that is both a homeomorphism and a monoid homomorphism preserves the "continuousness" of the operation. (Contributed by Thierry Arnoux, 25-Mar-2017.) |
| ⊢ 𝐹 ∈ (𝐽Homeo𝐾) & ⊢ + :(𝐵 × 𝐵)⟶𝐵 & ⊢ ∗ :(𝐶 × 𝐶)⟶𝐶 & ⊢ 𝐽 ∈ (TopOn‘𝐵) & ⊢ 𝐾 ∈ (TopOn‘𝐶) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ∗ (𝐹‘𝑦))) & ⊢ + ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ⇒ ⊢ ∗ ∈ ((𝐾 ×t 𝐾) Cn 𝐾) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |