HomeTheorem List (p. 325 of 473)
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. 325 of 473) | < 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-29860) |
Hilbert Space Explorer
(29861-31383) |
Users' Mathboxes
(31384-47242) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | lmat22e21 32401 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
| ⊢ 𝑀 = (litMat‘⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (2𝑀1) = 𝐶) | ||
| Theorem | lmat22e22 32402 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
| ⊢ 𝑀 = (litMat‘⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (2𝑀2) = 𝐷) | ||
| Theorem | lmat22det 32403 | The determinant of a literal 2x2 complex matrix. (Contributed by Thierry Arnoux, 1-Sep-2020.) |
| ⊢ 𝑀 = (litMat‘⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ · = (.r‘𝑅) & ⊢ − = (-g‘𝑅) & ⊢ 𝑉 = (Base‘𝑅) & ⊢ 𝐽 = ((1...2) maDet 𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → (𝐽‘𝑀) = ((𝐴 · 𝐷) − (𝐶 · 𝐵))) | ||
| Theorem | mdetpmtr1 32404* | The determinant of a matrix with permuted rows is the determinant of the original matrix multiplied by the sign of the permutation. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐺 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐸 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀𝑗)) ⇒ ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝑀) = (((𝑍 ∘ 𝑆)‘𝑃) · (𝐷‘𝐸))) | ||
| Theorem | mdetpmtr2 32405* | The determinant of a matrix with permuted columns is the determinant of the original matrix multiplied by the sign of the permutation. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐺 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐸 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑖𝑀(𝑃‘𝑗))) ⇒ ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝑀) = (((𝑍 ∘ 𝑆)‘𝑃) · (𝐷‘𝐸))) | ||
| Theorem | mdetpmtr12 32406* | The determinant of a matrix with permuted rows and columns is the determinant of the original matrix multiplied by the product of the signs of the permutations. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐺 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐸 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀(𝑄‘𝑗))) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) & ⊢ (𝜑 → 𝑃 ∈ 𝐺) & ⊢ (𝜑 → 𝑄 ∈ 𝐺) ⇒ ⊢ (𝜑 → (𝐷‘𝑀) = ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐷‘𝐸))) | ||
| Theorem | mdetlap1 32407* | A Laplace expansion of the determinant of a matrix, using the adjunct (cofactor) matrix. (Contributed by Thierry Arnoux, 16-Aug-2020.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐾 = (𝑁 maAdju 𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝐼 ∈ 𝑁) → (𝐷‘𝑀) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝐼𝑀𝑗) · (𝑗(𝐾‘𝑀)𝐼))))) | ||
| Theorem | madjusmdetlem1 32408* | Lemma for madjusmdet 32412. (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 32409* | Lemma for madjusmdet 32412. (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 32410* | Lemma for madjusmdet 32412. (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 32411* | Lemma for madjusmdet 32412. (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 32412 | 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 32413* | 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 32414* | The predicate "is a T0 space", using closed sets. (Contributed by Thierry Arnoux, 16-Aug-2020.) |
| ⊢ (𝜑 → 𝐵 = ∪ 𝐽) & ⊢ (𝜑 → 𝐷 = (Clsd‘𝐽)) ⇒ ⊢ (𝜑 → (𝐽 ∈ Kol2 ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∀𝑑 ∈ 𝐷 (𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑) → 𝑥 = 𝑦)))) | ||
| Theorem | txomap 32415* | 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 32416* | 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 32417* | 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 32418* | 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 32419* | 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 32420* | 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 10424. (Contributed by Thierry Arnoux, 12-Jan-2020.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴Ref𝐵 ↔ (∪ 𝐵 ⊆ ∪ 𝐴 ∧ ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑣 ∈ 𝐴 𝑣 ⊆ (𝑓‘𝑣))))) | ||
| Theorem | locfinreflem 32421* | 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 32422* | 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 32423 | The "every open cover has an 𝐴 refinement" predicate. |
| class CovHasRef𝐴 | ||
| Definition | df-cref 32424* | 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 32425* | 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 32426 | Equality theorem for the "every open cover has an A refinement" predicate. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ (𝐴 = 𝐵 → CovHasRef𝐴 = CovHasRef𝐵) | ||
| Theorem | creftop 32427 | A space where every open cover has an 𝐴 refinement is a topological space. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ (𝐽 ∈ CovHasRef𝐴 → 𝐽 ∈ Top) | ||
| Theorem | crefi 32428* | The property that every open cover has an 𝐴 refinement for the topological space 𝐽. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ CovHasRef𝐴 ∧ 𝐶 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝐶) → ∃𝑧 ∈ (𝒫 𝐽 ∩ 𝐴)𝑧Ref𝐶) | ||
| Theorem | crefdf 32429* | A formulation of crefi 32428 easier to use for definitions. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐵 = CovHasRef𝐴 & ⊢ (𝑧 ∈ 𝐴 → 𝜑) ⇒ ⊢ ((𝐽 ∈ 𝐵 ∧ 𝐶 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝐶) → ∃𝑧 ∈ 𝒫 𝐽(𝜑 ∧ 𝑧Ref𝐶)) | ||
| Theorem | crefss 32430 | The "every open cover has an 𝐴 refinement" predicate respects inclusion. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ (𝐴 ⊆ 𝐵 → CovHasRef𝐴 ⊆ CovHasRef𝐵) | ||
| Theorem | cmpcref 32431 | 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 32432* | Every open cover of a Compact space has a finite refinement. (Contributed by Thierry Arnoux, 1-Feb-2020.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Comp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈) → ∃𝑣 ∈ 𝒫 𝐽(𝑣 ∈ Fin ∧ 𝑣Ref𝑈)) | ||
| Syntax | cldlf 32433 | Extend class notation with the class of all Lindelöf spaces. |
| class Ldlf | ||
| Definition | df-ldlf 32434 | 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 32435* | Every open cover of a Lindelöf space has a countable refinement. (Contributed by Thierry Arnoux, 1-Feb-2020.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Ldlf ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈) → ∃𝑣 ∈ 𝒫 𝐽(𝑣 ≼ ω ∧ 𝑣Ref𝑈)) | ||
| Syntax | cpcmp 32436 | Extend class notation with the class of all paracompact topologies. |
| class Paracomp | ||
| Definition | df-pcmp 32437 | 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 32438 | The predicate "is a paracompact topology". (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ (𝐽 ∈ Paracomp ↔ 𝐽 ∈ CovHasRef(LocFin‘𝐽)) | ||
| Theorem | cmppcmp 32439 | Every compact space is paracompact. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ (𝐽 ∈ Comp → 𝐽 ∈ Paracomp) | ||
| Theorem | dispcmp 32440 | Every discrete space is paracompact. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ Paracomp) | ||
| Theorem | pcmplfin 32441* | 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 32442* | 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 32449 for the definition of 𝑉). The closed sets of the topology are in the range of 𝑉 (see zartopon 32458). The correspondence with the open sets is made in zarcls 32455. As proved in zart0 32460, the Zariski topology is T0 , but generally not T1 . | ||
| Syntax | crspec 32443 | Extend class notation with the spectrum of a ring. |
| class Spec | ||
| Definition | df-rspec 32444 | Define the spectrum of a ring. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| ⊢ Spec = (𝑟 ∈ Ring ↦ ((IDLsrg‘𝑟) ↾s (PrmIdeal‘𝑟))) | ||
| Theorem | rspecval 32445 | 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 32446 | 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 32447* | Topology component of the spectrum of a ring. (Contributed by Thierry Arnoux, 2-Jun-2024.) |
| ⊢ 𝑆 = (Spec‘𝑅) & ⊢ 𝐼 = (LIdeal‘𝑅) & ⊢ 𝐽 = ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) ⇒ ⊢ (𝑅 ∈ Ring → 𝐽 = (TopSet‘𝑆)) | ||
| Theorem | rspectopn 32448* | The topology component of the spectrum of a ring. (Contributed by Thierry Arnoux, 4-Jun-2024.) |
| ⊢ 𝑆 = (Spec‘𝑅) & ⊢ 𝐼 = (LIdeal‘𝑅) & ⊢ 𝑃 = (PrmIdeal‘𝑅) & ⊢ 𝐽 = ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝑃 ∣ ¬ 𝑖 ⊆ 𝑗}) ⇒ ⊢ (𝑅 ∈ Ring → 𝐽 = (TopOpen‘𝑆)) | ||
| Theorem | zarcls0 32449* | 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 32450* | 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 32451* | 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 32452* | 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 32453* | 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 32454* | The closed points of Zariski topology are the maximal ideals. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
| ⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) & ⊢ 𝐵 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ({𝑀} = (𝑉‘𝑀) ↔ 𝑀 ∈ (MaxIdeal‘𝑅))) | ||
| Theorem | zarcls 32455* | 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 32456* | 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 32457 | 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 32458 | The points of the Zariski topology are the prime ideals. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
| ⊢ 𝑆 = (Spec‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑆) & ⊢ 𝑃 = (PrmIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → 𝐽 ∈ (TopOn‘𝑃)) | ||
| Theorem | zar0ring 32459 | The Zariski Topology of the trivial ring. (Contributed by Thierry Arnoux, 1-Jul-2024.) |
| ⊢ 𝑆 = (Spec‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑆) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (♯‘𝐵) = 1) → 𝐽 = {∅}) | ||
| Theorem | zart0 32460 | 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 32461 | The Zariski topology restricted to maximal ideals is T1 . (Contributed by Thierry Arnoux, 16-Jun-2024.) |
| ⊢ 𝑆 = (Spec‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑆) & ⊢ 𝑀 = (MaxIdeal‘𝑅) & ⊢ 𝑇 = (𝐽 ↾t 𝑀) ⇒ ⊢ (𝑅 ∈ CRing → 𝑇 ∈ Fre) | ||
| Theorem | zarcmplem 32462* | Lemma for zarcmp 32463. (Contributed by Thierry Arnoux, 2-Jul-2024.) |
| ⊢ 𝑆 = (Spec‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑆) & ⊢ 𝑉 = (𝑖 ∈ (LIdeal‘𝑅) ↦ {𝑗 ∈ (PrmIdeal‘𝑅) ∣ 𝑖 ⊆ 𝑗}) ⇒ ⊢ (𝑅 ∈ CRing → 𝐽 ∈ Comp) | ||
| Theorem | zarcmp 32463 | 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 32464 | The spectrum of a ring 𝑅 is a topological space. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
| ⊢ 𝑆 = (Spec‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → 𝑆 ∈ TopSp) | ||
| Theorem | rhmpreimacnlem 32465* | Lemma for rhmpreimacn 32466. (Contributed by Thierry Arnoux, 7-Jul-2024.) |
| ⊢ 𝑇 = (Spec‘𝑅) & ⊢ 𝑈 = (Spec‘𝑆) & ⊢ 𝐴 = (PrmIdeal‘𝑅) & ⊢ 𝐵 = (PrmIdeal‘𝑆) & ⊢ 𝐽 = (TopOpen‘𝑇) & ⊢ 𝐾 = (TopOpen‘𝑈) & ⊢ 𝐺 = (𝑖 ∈ 𝐵 ↦ (◡𝐹 “ 𝑖)) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ CRing) & ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆)) & ⊢ (𝜑 → ran 𝐹 = (Base‘𝑆)) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ 𝑉 = (𝑗 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑗 ⊆ 𝑘}) & ⊢ 𝑊 = (𝑗 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑗 ⊆ 𝑘}) ⇒ ⊢ (𝜑 → (𝑊‘(𝐹 “ 𝐼)) = (◡𝐺 “ (𝑉‘𝐼))) | ||
| Theorem | rhmpreimacn 32466* | 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 32467 | Extend class notation with the class of metric identifications. |
| class ~Met | ||
| Syntax | cpstm 32468 | Extend class notation with the metric induced by a pseudometric. |
| class pstoMet | ||
| Definition | df-metid 32469* | 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 32470* | 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 32471* | Value of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| ⊢ (𝐷 ∈ (PsMet‘𝑋) → (~Met‘𝐷) = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝑥𝐷𝑦) = 0)}) | ||
| Theorem | metidss 32472 | As a relation, the metric identification is a subset of a Cartesian product. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| ⊢ (𝐷 ∈ (PsMet‘𝑋) → (~Met‘𝐷) ⊆ (𝑋 × 𝑋)) | ||
| Theorem | metidv 32473 | 𝐴 and 𝐵 identify by the metric 𝐷 if their distance is zero. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴(~Met‘𝐷)𝐵 ↔ (𝐴𝐷𝐵) = 0)) | ||
| Theorem | metideq 32474 | Basic property of the metric identification relation. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐴𝐷𝐸) = (𝐵𝐷𝐹)) | ||
| Theorem | metider 32475 | The metric identification is an equivalence relation. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
| ⊢ (𝐷 ∈ (PsMet‘𝑋) → (~Met‘𝐷) Er 𝑋) | ||
| Theorem | pstmval 32476* | Value of the metric induced by a pseudometric 𝐷. (Contributed by Thierry Arnoux, 7-Feb-2018.) |
| ⊢ ∼ = (~Met‘𝐷) ⇒ ⊢ (𝐷 ∈ (PsMet‘𝑋) → (pstoMet‘𝐷) = (𝑎 ∈ (𝑋 / ∼ ), 𝑏 ∈ (𝑋 / ∼ ) ↦ ∪ {𝑧 ∣ ∃𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝑧 = (𝑥𝐷𝑦)})) | ||
| Theorem | pstmfval 32477 | Function value of the metric induced by a pseudometric 𝐷 (Contributed by Thierry Arnoux, 11-Feb-2018.) |
| ⊢ ∼ = (~Met‘𝐷) ⇒ ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ([𝐴] ∼ (pstoMet‘𝐷)[𝐵] ∼ ) = (𝐴𝐷𝐵)) | ||
| Theorem | pstmxmet 32478 | 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 32479 | 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 32480 | 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 32481 | 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 32482 | 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 32483 | 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 32484 | The union of the closed set is the underlying set of the topology. (Contributed by Thierry Arnoux, 21-Sep-2017.) |
| ⊢ 𝐽 ∈ Top & ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ∪ (Clsd‘𝐽) = 𝑋 | ||
| Theorem | tpr2tp 32485 | 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 32486 | 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 32487 | 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 32488 | 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 32489 | 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 32490 | 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 32491* | Lemma for cnre2csqima 32492. (Contributed by Thierry Arnoux, 27-Sep-2017.) |
| ⊢ (𝐺 ↾ (ℝ × ℝ)) = (𝐻 ∘ 𝐹) & ⊢ 𝐹 Fn (ℝ × ℝ) & ⊢ 𝐺 Fn V & ⊢ (𝑥 ∈ (ℝ × ℝ) → (𝐺‘𝑥) ∈ ℝ) & ⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → (𝐻‘(𝑥 − 𝑦)) = ((𝐻‘𝑥) − (𝐻‘𝑦))) ⇒ ⊢ ((𝑋 ∈ (ℝ × ℝ) ∧ 𝑌 ∈ (ℝ × ℝ) ∧ 𝐷 ∈ ℝ+) → (𝑌 ∈ (◡(𝐺 ↾ (ℝ × ℝ)) “ (((𝐺‘𝑋) − 𝐷)(,)((𝐺‘𝑋) + 𝐷))) → (abs‘(𝐻‘((𝐹‘𝑌) − (𝐹‘𝑋)))) < 𝐷)) | ||
| Theorem | cnre2csqima 32492* | 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 32493* | 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 32494* | 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 32495 | Domain of the relation of a proset. (Contributed by Thierry Arnoux, 11-Sep-2015.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ (𝐾 ∈ Proset → dom ≤ = 𝐵) | ||
| Theorem | prsrn 32496 | Range of the relation of a proset. (Contributed by Thierry Arnoux, 11-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ (𝐾 ∈ Proset → ran ≤ = 𝐵) | ||
| Theorem | prsss 32497 | Relation of a subproset. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → ( ≤ ∩ (𝐴 × 𝐴)) = ((le‘𝐾) ∩ (𝐴 × 𝐴))) | ||
| Theorem | prsssdm 32498 | Domain of a subproset relation. (Contributed by Thierry Arnoux, 12-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) ⇒ ⊢ ((𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵) → dom ( ≤ ∩ (𝐴 × 𝐴)) = 𝐴) | ||
| Theorem | ordtprsval 32499* | 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 32500* | Value of the order topology. (Contributed by Thierry Arnoux, 13-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = ((le‘𝐾) ∩ (𝐵 × 𝐵)) & ⊢ 𝐸 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥}) & ⊢ 𝐹 = ran (𝑥 ∈ 𝐵 ↦ {𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦}) ⇒ ⊢ (𝐾 ∈ Proset → 𝐵 = ∪ ({𝐵} ∪ (𝐸 ∪ 𝐹))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |