| Metamath
Proof Explorer Theorem List (p. 239 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | reghmph 23801 | Regularity is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.) |
| ⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Reg → 𝐾 ∈ Reg)) | ||
| Theorem | nrmhmph 23802 | Normality is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.) |
| ⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm)) | ||
| Theorem | hmph0 23803 | A topology homeomorphic to the empty set is empty. (Contributed by FL, 18-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
| ⊢ (𝐽 ≃ {∅} ↔ 𝐽 = {∅}) | ||
| Theorem | hmphdis 23804 | Homeomorphisms preserve topological discreteness. (Contributed by Mario Carneiro, 10-Sep-2015.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ≃ 𝒫 𝐴 → 𝐽 = 𝒫 𝑋) | ||
| Theorem | hmphindis 23805 | Homeomorphisms preserve topological indiscreteness. (Contributed by FL, 18-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ≃ {∅, 𝐴} → 𝐽 = {∅, 𝑋}) | ||
| Theorem | indishmph 23806 | Equinumerous sets equipped with their indiscrete topologies are homeomorphic (which means in that particular case that a segment is homeomorphic to a circle contrary to what Wikipedia claims). (Contributed by FL, 17-Aug-2008.) (Proof shortened by Mario Carneiro, 10-Sep-2015.) |
| ⊢ (𝐴 ≈ 𝐵 → {∅, 𝐴} ≃ {∅, 𝐵}) | ||
| Theorem | hmphen2 23807 | Homeomorphisms preserve the cardinality of the underlying sets. (Contributed by FL, 17-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
| ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ (𝐽 ≃ 𝐾 → 𝑋 ≈ 𝑌) | ||
| Theorem | cmphaushmeo 23808 | A continuous bijection from a compact space to a Hausdorff space is a homeomorphism. (Contributed by Mario Carneiro, 17-Feb-2015.) |
| ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ ((𝐽 ∈ Comp ∧ 𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 ∈ (𝐽Homeo𝐾) ↔ 𝐹:𝑋–1-1-onto→𝑌)) | ||
| Theorem | ordthmeolem 23809 | Lemma for ordthmeo 23810. (Contributed by Mario Carneiro, 9-Sep-2015.) |
| ⊢ 𝑋 = dom 𝑅 & ⊢ 𝑌 = dom 𝑆 ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝐹 ∈ ((ordTop‘𝑅) Cn (ordTop‘𝑆))) | ||
| Theorem | ordthmeo 23810 | An order isomorphism is a homeomorphism on the respective order topologies. (Contributed by Mario Carneiro, 9-Sep-2015.) |
| ⊢ 𝑋 = dom 𝑅 & ⊢ 𝑌 = dom 𝑆 ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝐹 ∈ ((ordTop‘𝑅)Homeo(ordTop‘𝑆))) | ||
| Theorem | txhmeo 23811* | Lift a pair of homeomorphisms on the factors to a homeomorphism of product topologies. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 & ⊢ (𝜑 → 𝐹 ∈ (𝐽Homeo𝐿)) & ⊢ (𝜑 → 𝐺 ∈ (𝐾Homeo𝑀)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑦)〉) ∈ ((𝐽 ×t 𝐾)Homeo(𝐿 ×t 𝑀))) | ||
| Theorem | txswaphmeolem 23812* | Show inverse for the "swap components" operation on a Cartesian product. (Contributed by Mario Carneiro, 21-Mar-2015.) |
| ⊢ ((𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 〈𝑥, 𝑦〉) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈𝑦, 𝑥〉)) = ( I ↾ (𝑋 × 𝑌)) | ||
| Theorem | txswaphmeo 23813* | There is a homeomorphism from 𝑋 × 𝑌 to 𝑌 × 𝑋. (Contributed by Mario Carneiro, 21-Mar-2015.) |
| ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈𝑦, 𝑥〉) ∈ ((𝐽 ×t 𝐾)Homeo(𝐾 ×t 𝐽))) | ||
| Theorem | pt1hmeo 23814* | The canonical homeomorphism from a topological product on a singleton to the topology of the factor. (Contributed by Mario Carneiro, 3-Feb-2015.) (Proof shortened by AV, 18-Apr-2021.) |
| ⊢ 𝐾 = (∏t‘{〈𝐴, 𝐽〉}) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ {〈𝐴, 𝑥〉}) ∈ (𝐽Homeo𝐾)) | ||
| Theorem | ptuncnv 23815* | Exhibit the converse function of the map 𝐺 which joins two product topologies on disjoint index sets. (Contributed by Mario Carneiro, 8-Feb-2015.) (Proof shortened by Mario Carneiro, 23-Aug-2015.) |
| ⊢ 𝑋 = ∪ 𝐾 & ⊢ 𝑌 = ∪ 𝐿 & ⊢ 𝐽 = (∏t‘𝐹) & ⊢ 𝐾 = (∏t‘(𝐹 ↾ 𝐴)) & ⊢ 𝐿 = (∏t‘(𝐹 ↾ 𝐵)) & ⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥 ∪ 𝑦)) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐶⟶Top) & ⊢ (𝜑 → 𝐶 = (𝐴 ∪ 𝐵)) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) ⇒ ⊢ (𝜑 → ◡𝐺 = (𝑧 ∈ ∪ 𝐽 ↦ 〈(𝑧 ↾ 𝐴), (𝑧 ↾ 𝐵)〉)) | ||
| Theorem | ptunhmeo 23816* | Define a homeomorphism from a binary product of indexed product topologies to an indexed product topology on the union of the index sets. This is the topological analogue of (𝐴↑𝐵) · (𝐴↑𝐶) = 𝐴↑(𝐵 + 𝐶). (Contributed by Mario Carneiro, 8-Feb-2015.) (Proof shortened by Mario Carneiro, 23-Aug-2015.) |
| ⊢ 𝑋 = ∪ 𝐾 & ⊢ 𝑌 = ∪ 𝐿 & ⊢ 𝐽 = (∏t‘𝐹) & ⊢ 𝐾 = (∏t‘(𝐹 ↾ 𝐴)) & ⊢ 𝐿 = (∏t‘(𝐹 ↾ 𝐵)) & ⊢ 𝐺 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝑥 ∪ 𝑦)) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐶⟶Top) & ⊢ (𝜑 → 𝐶 = (𝐴 ∪ 𝐵)) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) ⇒ ⊢ (𝜑 → 𝐺 ∈ ((𝐾 ×t 𝐿)Homeo𝐽)) | ||
| Theorem | xpstopnlem1 23817* | The function 𝐹 used in xpsval 17615 is a homeomorphism from the binary product topology to the indexed product topology. (Contributed by Mario Carneiro, 2-Sep-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) ⇒ ⊢ (𝜑 → 𝐹 ∈ ((𝐽 ×t 𝐾)Homeo(∏t‘{〈∅, 𝐽〉, 〈1o, 𝐾〉}))) | ||
| Theorem | xpstps 23818 | A binary product of topologies is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.) |
| ⊢ 𝑇 = (𝑅 ×s 𝑆) ⇒ ⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝑇 ∈ TopSp) | ||
| Theorem | xpstopnlem2 23819* | Lemma for xpstopn 23820. (Contributed by Mario Carneiro, 27-Aug-2015.) |
| ⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝐽 = (TopOpen‘𝑅) & ⊢ 𝐾 = (TopOpen‘𝑆) & ⊢ 𝑂 = (TopOpen‘𝑇) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) ⇒ ⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝑂 = (𝐽 ×t 𝐾)) | ||
| Theorem | xpstopn 23820 | The topology on a binary product of topological spaces, as we have defined it (transferring the indexed product topology on functions on {∅, 1o} to (𝑋 × 𝑌) by the canonical bijection), coincides with the usual topological product (generated by a base of rectangles). (Contributed by Mario Carneiro, 27-Aug-2015.) |
| ⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝐽 = (TopOpen‘𝑅) & ⊢ 𝐾 = (TopOpen‘𝑆) & ⊢ 𝑂 = (TopOpen‘𝑇) ⇒ ⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝑂 = (𝐽 ×t 𝐾)) | ||
| Theorem | ptcmpfi 23821 | A topological product of finitely many compact spaces is compact. This weak version of Tychonoff's theorem does not require the axiom of choice. (Contributed by Mario Carneiro, 8-Feb-2015.) |
| ⊢ ((𝐴 ∈ Fin ∧ 𝐹:𝐴⟶Comp) → (∏t‘𝐹) ∈ Comp) | ||
| Theorem | xkocnv 23822* | The inverse of the "currying" function 𝐹 is the uncurrying function. (Contributed by Mario Carneiro, 13-Apr-2015.) |
| ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ 𝐹 = (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↦ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) & ⊢ (𝜑 → 𝐽 ∈ 𝑛-Locally Comp) & ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally Comp) & ⊢ (𝜑 → 𝐿 ∈ Top) ⇒ ⊢ (𝜑 → ◡𝐹 = (𝑔 ∈ (𝐽 Cn (𝐿 ↑ko 𝐾)) ↦ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ((𝑔‘𝑥)‘𝑦)))) | ||
| Theorem | xkohmeo 23823* | The Exponential Law for topological spaces. The "currying" function 𝐹 is a homeomorphism on function spaces when 𝐽 and 𝐾 are exponentiable spaces (by xkococn 23668, it is sufficient to assume that 𝐽, 𝐾 are locally compact to ensure exponentiability). (Contributed by Mario Carneiro, 13-Apr-2015.) (Proof shortened by Mario Carneiro, 23-Aug-2015.) |
| ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ 𝐹 = (𝑓 ∈ ((𝐽 ×t 𝐾) Cn 𝐿) ↦ (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ (𝑥𝑓𝑦)))) & ⊢ (𝜑 → 𝐽 ∈ 𝑛-Locally Comp) & ⊢ (𝜑 → 𝐾 ∈ 𝑛-Locally Comp) & ⊢ (𝜑 → 𝐿 ∈ Top) ⇒ ⊢ (𝜑 → 𝐹 ∈ ((𝐿 ↑ko (𝐽 ×t 𝐾))Homeo((𝐿 ↑ko 𝐾) ↑ko 𝐽))) | ||
| Theorem | qtopf1 23824 | If a quotient map is injective, then it is a homeomorphism. (Contributed by Mario Carneiro, 25-Aug-2015.) |
| ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐹:𝑋–1-1→𝑌) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐽Homeo(𝐽 qTop 𝐹))) | ||
| Theorem | qtophmeo 23825* | If two functions on a base topology 𝐽 make the same identifications in order to create quotient spaces 𝐽 qTop 𝐹 and 𝐽 qTop 𝐺, then not only are 𝐽 qTop 𝐹 and 𝐽 qTop 𝐺 homeomorphic, but there is a unique homeomorphism that makes the diagram commute. (Contributed by Mario Carneiro, 24-Mar-2015.) (Proof shortened by Mario Carneiro, 23-Aug-2015.) |
| ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) & ⊢ (𝜑 → 𝐺:𝑋–onto→𝑌) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝐺‘𝑥) = (𝐺‘𝑦))) ⇒ ⊢ (𝜑 → ∃!𝑓 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺))𝐺 = (𝑓 ∘ 𝐹)) | ||
| Theorem | t0kq 23826* | A topological space is T0 iff the quotient map is a homeomorphism onto the space's Kolmogorov quotient. (Contributed by Mario Carneiro, 25-Aug-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ {𝑦 ∈ 𝐽 ∣ 𝑥 ∈ 𝑦}) ⇒ ⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ∈ Kol2 ↔ 𝐹 ∈ (𝐽Homeo(KQ‘𝐽)))) | ||
| Theorem | kqhmph 23827 | A topological space is T0 iff it is homeomorphic to its Kolmogorov quotient. (Contributed by Mario Carneiro, 25-Aug-2015.) |
| ⊢ (𝐽 ∈ Kol2 ↔ 𝐽 ≃ (KQ‘𝐽)) | ||
| Theorem | ist1-5lem 23828 | Lemma for ist1-5 23830 and similar theorems. If 𝐴 is a topological property which implies T0, such as T1 or T2, the property can be "decomposed" into T0 and a non-T0 version of property 𝐴 (which is defined as stating that the Kolmogorov quotient of the space has property 𝐴). For example, if 𝐴 is T1, then the theorem states that a space is T1 iff it is T0 and its Kolmogorov quotient is T1 (we call this property R0). (Contributed by Mario Carneiro, 25-Aug-2015.) |
| ⊢ (𝐽 ∈ 𝐴 → 𝐽 ∈ Kol2) & ⊢ (𝐽 ≃ (KQ‘𝐽) → (𝐽 ∈ 𝐴 → (KQ‘𝐽) ∈ 𝐴)) & ⊢ ((KQ‘𝐽) ≃ 𝐽 → ((KQ‘𝐽) ∈ 𝐴 → 𝐽 ∈ 𝐴)) ⇒ ⊢ (𝐽 ∈ 𝐴 ↔ (𝐽 ∈ Kol2 ∧ (KQ‘𝐽) ∈ 𝐴)) | ||
| Theorem | t1r0 23829 | A T1 space is R0. That is, the Kolmogorov quotient of a T1 space is also T1 (because they are homeomorphic). (Contributed by Mario Carneiro, 25-Aug-2015.) |
| ⊢ (𝐽 ∈ Fre → (KQ‘𝐽) ∈ Fre) | ||
| Theorem | ist1-5 23830 | A topological space is T1 iff it is both T0 and R0. (Contributed by Mario Carneiro, 25-Aug-2015.) |
| ⊢ (𝐽 ∈ Fre ↔ (𝐽 ∈ Kol2 ∧ (KQ‘𝐽) ∈ Fre)) | ||
| Theorem | ishaus3 23831 | A topological space is Hausdorff iff it is both T0 and R1 (where R1 means that any two topologically distinct points are separated by neighborhoods). (Contributed by Mario Carneiro, 25-Aug-2015.) |
| ⊢ (𝐽 ∈ Haus ↔ (𝐽 ∈ Kol2 ∧ (KQ‘𝐽) ∈ Haus)) | ||
| Theorem | nrmreg 23832 | A normal T1 space is regular Hausdorff. In other words, a T4 space is T3 . One can get away with slightly weaker assumptions; see nrmr0reg 23757. (Contributed by Mario Carneiro, 25-Aug-2015.) |
| ⊢ ((𝐽 ∈ Nrm ∧ 𝐽 ∈ Fre) → 𝐽 ∈ Reg) | ||
| Theorem | reghaus 23833 | A regular T0 space is Hausdorff. In other words, a T3 space is T2 . A regular Hausdorff or T0 space is also known as a T3 space. (Contributed by Mario Carneiro, 24-Aug-2015.) |
| ⊢ (𝐽 ∈ Reg → (𝐽 ∈ Haus ↔ 𝐽 ∈ Kol2)) | ||
| Theorem | nrmhaus 23834 | A T1 normal space is Hausdorff. A Hausdorff or T1 normal space is also known as a T4 space. (Contributed by Mario Carneiro, 24-Aug-2015.) |
| ⊢ (𝐽 ∈ Nrm → (𝐽 ∈ Haus ↔ 𝐽 ∈ Fre)) | ||
| Theorem | elmptrab 23835* | Membership in a one-parameter class of sets. (Contributed by Stefan O'Rear, 28-Jul-2015.) |
| ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ {𝑦 ∈ 𝐵 ∣ 𝜑}) & ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶) & ⊢ (𝑥 ∈ 𝐷 → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝑌 ∈ (𝐹‘𝑋) ↔ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓)) | ||
| Theorem | elmptrab2 23836* | Membership in a one-parameter class of sets, indexed by arbitrary base sets. (Contributed by Stefan O'Rear, 28-Jul-2015.) (Revised by AV, 26-Mar-2021.) |
| ⊢ 𝐹 = (𝑥 ∈ V ↦ {𝑦 ∈ 𝐵 ∣ 𝜑}) & ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶) & ⊢ 𝐵 ∈ V & ⊢ (𝑌 ∈ 𝐶 → 𝑋 ∈ 𝑊) ⇒ ⊢ (𝑌 ∈ (𝐹‘𝑋) ↔ (𝑌 ∈ 𝐶 ∧ 𝜓)) | ||
| Theorem | isfbas 23837* | The predicate "𝐹 is a filter base." Note that some authors require filter bases to be closed under pairwise intersections, but that is not necessary under our definition. One advantage of this definition is that tails in a directed set form a filter base under our meaning. (Contributed by Jeff Hankins, 1-Sep-2009.) (Revised by Mario Carneiro, 28-Jul-2015.) |
| ⊢ (𝐵 ∈ 𝐴 → (𝐹 ∈ (fBas‘𝐵) ↔ (𝐹 ⊆ 𝒫 𝐵 ∧ (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝐹 ∩ 𝒫 (𝑥 ∩ 𝑦)) ≠ ∅)))) | ||
| Theorem | fbasne0 23838 | There are no empty filter bases. (Contributed by Jeff Hankins, 1-Sep-2009.) (Revised by Mario Carneiro, 28-Jul-2015.) |
| ⊢ (𝐹 ∈ (fBas‘𝐵) → 𝐹 ≠ ∅) | ||
| Theorem | 0nelfb 23839 | No filter base contains the empty set. (Contributed by Jeff Hankins, 1-Sep-2009.) (Revised by Mario Carneiro, 28-Jul-2015.) |
| ⊢ (𝐹 ∈ (fBas‘𝐵) → ¬ ∅ ∈ 𝐹) | ||
| Theorem | fbsspw 23840 | A filter base on a set is a subset of the power set. (Contributed by Stefan O'Rear, 28-Jul-2015.) |
| ⊢ (𝐹 ∈ (fBas‘𝐵) → 𝐹 ⊆ 𝒫 𝐵) | ||
| Theorem | fbelss 23841 | An element of the filter base is a subset of the base set. (Contributed by Stefan O'Rear, 28-Jul-2015.) |
| ⊢ ((𝐹 ∈ (fBas‘𝐵) ∧ 𝑋 ∈ 𝐹) → 𝑋 ⊆ 𝐵) | ||
| Theorem | fbdmn0 23842 | The domain of a filter base is nonempty. (Contributed by Mario Carneiro, 28-Nov-2013.) (Revised by Stefan O'Rear, 28-Jul-2015.) |
| ⊢ (𝐹 ∈ (fBas‘𝐵) → 𝐵 ≠ ∅) | ||
| Theorem | isfbas2 23843* | The predicate "𝐹 is a filter base." (Contributed by Jeff Hankins, 1-Sep-2009.) (Revised by Stefan O'Rear, 28-Jul-2015.) |
| ⊢ (𝐵 ∈ 𝐴 → (𝐹 ∈ (fBas‘𝐵) ↔ (𝐹 ⊆ 𝒫 𝐵 ∧ (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦))))) | ||
| Theorem | fbasssin 23844* | A filter base contains subsets of its pairwise intersections. (Contributed by Jeff Hankins, 1-Sep-2009.) (Revised by Jeff Hankins, 1-Dec-2010.) |
| ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹) → ∃𝑥 ∈ 𝐹 𝑥 ⊆ (𝐴 ∩ 𝐵)) | ||
| Theorem | fbssfi 23845* | A filter base contains subsets of its finite intersections. (Contributed by Mario Carneiro, 26-Nov-2013.) (Revised by Stefan O'Rear, 28-Jul-2015.) |
| ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝐴 ∈ (fi‘𝐹)) → ∃𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴) | ||
| Theorem | fbssint 23846* | A filter base contains subsets of its finite intersections. (Contributed by Jeff Hankins, 1-Sep-2009.) (Revised by Stefan O'Rear, 28-Jul-2015.) |
| ⊢ ((𝐹 ∈ (fBas‘𝐵) ∧ 𝐴 ⊆ 𝐹 ∧ 𝐴 ∈ Fin) → ∃𝑥 ∈ 𝐹 𝑥 ⊆ ∩ 𝐴) | ||
| Theorem | fbncp 23847 | A filter base does not contain complements of its elements. (Contributed by Mario Carneiro, 26-Nov-2013.) (Revised by Stefan O'Rear, 28-Jul-2015.) |
| ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝐴 ∈ 𝐹) → ¬ (𝐵 ∖ 𝐴) ∈ 𝐹) | ||
| Theorem | fbun 23848* | A necessary and sufficient condition for the union of two filter bases to also be a filter base. (Contributed by Mario Carneiro, 28-Nov-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
| ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝐺 ∈ (fBas‘𝑋)) → ((𝐹 ∪ 𝐺) ∈ (fBas‘𝑋) ↔ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐺 ∃𝑧 ∈ (𝐹 ∪ 𝐺)𝑧 ⊆ (𝑥 ∩ 𝑦))) | ||
| Theorem | fbfinnfr 23849 | No filter base containing a finite element is free. (Contributed by Jeff Hankins, 5-Dec-2009.) (Revised by Stefan O'Rear, 28-Jul-2015.) |
| ⊢ ((𝐹 ∈ (fBas‘𝐵) ∧ 𝑆 ∈ 𝐹 ∧ 𝑆 ∈ Fin) → ∩ 𝐹 ≠ ∅) | ||
| Theorem | opnfbas 23850* | The collection of open supersets of a nonempty set in a topology is a neighborhoods of the set, one of the motivations for the filter concept. (Contributed by Jeff Hankins, 2-Sep-2009.) (Revised by Mario Carneiro, 7-Aug-2015.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → {𝑥 ∈ 𝐽 ∣ 𝑆 ⊆ 𝑥} ∈ (fBas‘𝑋)) | ||
| Theorem | trfbas2 23851 | Conditions for the trace of a filter base 𝐹 to be a filter base. (Contributed by Mario Carneiro, 13-Oct-2015.) |
| ⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝐹 ↾t 𝐴) ∈ (fBas‘𝐴) ↔ ¬ ∅ ∈ (𝐹 ↾t 𝐴))) | ||
| Theorem | trfbas 23852* | Conditions for the trace of a filter base 𝐹 to be a filter base. (Contributed by Mario Carneiro, 13-Oct-2015.) |
| ⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝐹 ↾t 𝐴) ∈ (fBas‘𝐴) ↔ ∀𝑣 ∈ 𝐹 (𝑣 ∩ 𝐴) ≠ ∅)) | ||
| Syntax | cfil 23853 | Extend class notation with the set of filters on a set. |
| class Fil | ||
| Definition | df-fil 23854* | The set of filters on a set. Definition 1 (axioms FI, FIIa, FIIb, FIII) of [BourbakiTop1] p. I.36. Filters are used to define the concept of limit in the general case. They are a generalization of the idea of neighborhoods. Suppose you are in ℝ. With neighborhoods you can express the idea of a variable that tends to a specific number but you can't express the idea of a variable that tends to infinity. Filters relax the "axioms" of neighborhoods and then succeed in expressing the idea of something that tends to infinity. Filters were invented by Cartan in 1937 and made famous by Bourbaki in his treatise. A notion similar to the notion of filter is the concept of net invented by Moore and Smith in 1922. (Contributed by FL, 20-Jul-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.) |
| ⊢ Fil = (𝑧 ∈ V ↦ {𝑓 ∈ (fBas‘𝑧) ∣ ∀𝑥 ∈ 𝒫 𝑧((𝑓 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝑓)}) | ||
| Theorem | isfil 23855* | The predicate "is a filter." (Contributed by FL, 20-Jul-2007.) (Revised by Mario Carneiro, 28-Jul-2015.) |
| ⊢ (𝐹 ∈ (Fil‘𝑋) ↔ (𝐹 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ 𝒫 𝑋((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝐹))) | ||
| Theorem | filfbas 23856 | A filter is a filter base. (Contributed by Jeff Hankins, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Jul-2015.) |
| ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋)) | ||
| Theorem | 0nelfil 23857 | The empty set doesn't belong to a filter. (Contributed by FL, 20-Jul-2007.) (Revised by Mario Carneiro, 28-Jul-2015.) |
| ⊢ (𝐹 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝐹) | ||
| Theorem | fileln0 23858 | An element of a filter is nonempty. (Contributed by FL, 24-May-2011.) (Revised by Mario Carneiro, 28-Jul-2015.) |
| ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → 𝐴 ≠ ∅) | ||
| Theorem | filsspw 23859 | A filter is a subset of the power set of the base set. (Contributed by Stefan O'Rear, 28-Jul-2015.) |
| ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋) | ||
| Theorem | filelss 23860 | An element of a filter is a subset of the base set. (Contributed by Stefan O'Rear, 28-Jul-2015.) |
| ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → 𝐴 ⊆ 𝑋) | ||
| Theorem | filss 23861 | A filter is closed under taking supersets. (Contributed by FL, 20-Jul-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.) |
| ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ⊆ 𝑋 ∧ 𝐴 ⊆ 𝐵)) → 𝐵 ∈ 𝐹) | ||
| Theorem | filin 23862 | A filter is closed under taking intersections. (Contributed by FL, 20-Jul-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.) |
| ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹) → (𝐴 ∩ 𝐵) ∈ 𝐹) | ||
| Theorem | filtop 23863 | The underlying set belongs to the filter. (Contributed by FL, 20-Jul-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.) |
| ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹) | ||
| Theorem | isfil2 23864* | Derive the standard axioms of a filter. (Contributed by Mario Carneiro, 27-Nov-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
| ⊢ (𝐹 ∈ (Fil‘𝑋) ↔ ((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹)) | ||
| Theorem | isfildlem 23865* | Lemma for isfild 23866. (Contributed by Mario Carneiro, 1-Dec-2013.) |
| ⊢ (𝜑 → (𝑥 ∈ 𝐹 ↔ (𝑥 ⊆ 𝐴 ∧ 𝜓))) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐵 ∈ 𝐹 ↔ (𝐵 ⊆ 𝐴 ∧ [𝐵 / 𝑥]𝜓))) | ||
| Theorem | isfild 23866* | Sufficient condition for a set of the form {𝑥 ∈ 𝒫 𝐴 ∣ 𝜑} to be a filter. (Contributed by Mario Carneiro, 1-Dec-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.) (Revised by AV, 10-Apr-2024.) |
| ⊢ (𝜑 → (𝑥 ∈ 𝐹 ↔ (𝑥 ⊆ 𝐴 ∧ 𝜓))) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → [𝐴 / 𝑥]𝜓) & ⊢ (𝜑 → ¬ [∅ / 𝑥]𝜓) & ⊢ ((𝜑 ∧ 𝑦 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝑦) → ([𝑧 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜓)) & ⊢ ((𝜑 ∧ 𝑦 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝐴) → (([𝑦 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜓) → [(𝑦 ∩ 𝑧) / 𝑥]𝜓)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (Fil‘𝐴)) | ||
| Theorem | filfi 23867 | A filter is closed under taking intersections. (Contributed by Mario Carneiro, 27-Nov-2013.) (Revised by Stefan O'Rear, 28-Jul-2015.) |
| ⊢ (𝐹 ∈ (Fil‘𝑋) → (fi‘𝐹) = 𝐹) | ||
| Theorem | filinn0 23868 | The intersection of two elements of a filter can't be empty. (Contributed by FL, 16-Sep-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.) |
| ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹) → (𝐴 ∩ 𝐵) ≠ ∅) | ||
| Theorem | filintn0 23869 | A filter has the finite intersection property. Remark below Definition 1 of [BourbakiTop1] p. I.36. (Contributed by FL, 20-Sep-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.) |
| ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐴 ⊆ 𝐹 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin)) → ∩ 𝐴 ≠ ∅) | ||
| Theorem | filn0 23870 | The empty set is not a filter. Remark below Definition 1 of [BourbakiTop1] p. I.36. (Contributed by FL, 30-Oct-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.) |
| ⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ≠ ∅) | ||
| Theorem | infil 23871 | The intersection of two filters is a filter. Use fiint 9366 to extend this property to the intersection of a finite set of filters. Paragraph 3 of [BourbakiTop1] p. I.36. (Contributed by FL, 17-Sep-2007.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
| ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐺 ∈ (Fil‘𝑋)) → (𝐹 ∩ 𝐺) ∈ (Fil‘𝑋)) | ||
| Theorem | snfil 23872 | A singleton is a filter. Example 1 of [BourbakiTop1] p. I.36. (Contributed by FL, 16-Sep-2007.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
| ⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅) → {𝐴} ∈ (Fil‘𝐴)) | ||
| Theorem | fbasweak 23873 | A filter base on any set is also a filter base on any larger set. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
| ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝐹 ⊆ 𝒫 𝑌 ∧ 𝑌 ∈ 𝑉) → 𝐹 ∈ (fBas‘𝑌)) | ||
| Theorem | snfbas 23874 | Condition for a singleton to be a filter base. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
| ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐵 ∈ 𝑉) → {𝐴} ∈ (fBas‘𝐵)) | ||
| Theorem | fsubbas 23875 | A condition for a set to generate a filter base. (Contributed by Jeff Hankins, 2-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
| ⊢ (𝑋 ∈ 𝑉 → ((fi‘𝐴) ∈ (fBas‘𝑋) ↔ (𝐴 ⊆ 𝒫 𝑋 ∧ 𝐴 ≠ ∅ ∧ ¬ ∅ ∈ (fi‘𝐴)))) | ||
| Theorem | fbasfip 23876 | A filter base has the finite intersection property. (Contributed by Jeff Hankins, 2-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
| ⊢ (𝐹 ∈ (fBas‘𝑋) → ¬ ∅ ∈ (fi‘𝐹)) | ||
| Theorem | fbunfip 23877* | A helpful lemma for showing that certain sets generate filters. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
| ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝐺 ∈ (fBas‘𝑌)) → (¬ ∅ ∈ (fi‘(𝐹 ∪ 𝐺)) ↔ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐺 (𝑥 ∩ 𝑦) ≠ ∅)) | ||
| Theorem | fgval 23878* | The filter generating class gives a filter for every filter base. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
| ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) = {𝑥 ∈ 𝒫 𝑋 ∣ (𝐹 ∩ 𝒫 𝑥) ≠ ∅}) | ||
| Theorem | elfg 23879* | A condition for elements of a generated filter. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
| ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝐴 ∈ (𝑋filGen𝐹) ↔ (𝐴 ⊆ 𝑋 ∧ ∃𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴))) | ||
| Theorem | ssfg 23880 | A filter base is a subset of its generated filter. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
| ⊢ (𝐹 ∈ (fBas‘𝑋) → 𝐹 ⊆ (𝑋filGen𝐹)) | ||
| Theorem | fgss 23881 | A bigger base generates a bigger filter. (Contributed by NM, 5-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
| ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝐺 ∈ (fBas‘𝑋) ∧ 𝐹 ⊆ 𝐺) → (𝑋filGen𝐹) ⊆ (𝑋filGen𝐺)) | ||
| Theorem | fgss2 23882* | A condition for a filter to be finer than another involving their filter bases. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
| ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ 𝐺 ∈ (fBas‘𝑋)) → ((𝑋filGen𝐹) ⊆ (𝑋filGen𝐺) ↔ ∀𝑥 ∈ 𝐹 ∃𝑦 ∈ 𝐺 𝑦 ⊆ 𝑥)) | ||
| Theorem | fgfil 23883 | A filter generates itself. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
| ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑋filGen𝐹) = 𝐹) | ||
| Theorem | elfilss 23884* | An element belongs to a filter iff any element below it does. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
| ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ 𝐹 ↔ ∃𝑡 ∈ 𝐹 𝑡 ⊆ 𝐴)) | ||
| Theorem | filfinnfr 23885 | No filter containing a finite element is free. (Contributed by Jeff Hankins, 5-Dec-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
| ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑆 ∈ 𝐹 ∧ 𝑆 ∈ Fin) → ∩ 𝐹 ≠ ∅) | ||
| Theorem | fgcl 23886 | A generated filter is a filter. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
| ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋)) | ||
| Theorem | fgabs 23887 | Absorption law for filter generation. (Contributed by Mario Carneiro, 15-Oct-2015.) |
| ⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹)) | ||
| Theorem | neifil 23888 | The neighborhoods of a nonempty set is a filter. Example 2 of [BourbakiTop1] p. I.36. (Contributed by FL, 18-Sep-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) |
| ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝑆 ≠ ∅) → ((nei‘𝐽)‘𝑆) ∈ (Fil‘𝑋)) | ||
| Theorem | filunibas 23889 | Recover the base set from a filter. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
| ⊢ (𝐹 ∈ (Fil‘𝑋) → ∪ 𝐹 = 𝑋) | ||
| Theorem | filunirn 23890 | Two ways to express a filter on an unspecified base. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
| ⊢ (𝐹 ∈ ∪ ran Fil ↔ 𝐹 ∈ (Fil‘∪ 𝐹)) | ||
| Theorem | filconn 23891 | A filter gives rise to a connected topology. (Contributed by Jeff Hankins, 6-Dec-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
| ⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {∅}) ∈ Conn) | ||
| Theorem | fbasrn 23892* | Given a filter on a domain, produce a filter on the range. (Contributed by Jeff Hankins, 7-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
| ⊢ 𝐶 = ran (𝑥 ∈ 𝐵 ↦ (𝐹 “ 𝑥)) ⇒ ⊢ ((𝐵 ∈ (fBas‘𝑋) ∧ 𝐹:𝑋⟶𝑌 ∧ 𝑌 ∈ 𝑉) → 𝐶 ∈ (fBas‘𝑌)) | ||
| Theorem | filuni 23893* | The union of a nonempty set of filters with a common base and closed under pairwise union is a filter. (Contributed by Mario Carneiro, 28-Nov-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
| ⊢ ((𝐹 ⊆ (Fil‘𝑋) ∧ 𝐹 ≠ ∅ ∧ ∀𝑓 ∈ 𝐹 ∀𝑔 ∈ 𝐹 (𝑓 ∪ 𝑔) ∈ 𝐹) → ∪ 𝐹 ∈ (Fil‘𝑋)) | ||
| Theorem | trfil1 23894 | Conditions for the trace of a filter 𝐿 to be a filter. (Contributed by FL, 2-Sep-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
| ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → 𝐴 = ∪ (𝐿 ↾t 𝐴)) | ||
| Theorem | trfil2 23895* | Conditions for the trace of a filter 𝐿 to be a filter. (Contributed by FL, 2-Sep-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
| ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ∀𝑣 ∈ 𝐿 (𝑣 ∩ 𝐴) ≠ ∅)) | ||
| Theorem | trfil3 23896 | Conditions for the trace of a filter 𝐿 to be a filter. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
| ⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ¬ (𝑌 ∖ 𝐴) ∈ 𝐿)) | ||
| Theorem | trfilss 23897 | If 𝐴 is a member of the filter, then the filter truncated to 𝐴 is a subset of the original filter. (Contributed by Mario Carneiro, 15-Oct-2015.) |
| ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → (𝐹 ↾t 𝐴) ⊆ 𝐹) | ||
| Theorem | fgtr 23898 | If 𝐴 is a member of the filter, then truncating 𝐹 to 𝐴 and regenerating the behavior outside 𝐴 using filGen recovers the original filter. (Contributed by Mario Carneiro, 15-Oct-2015.) |
| ⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → (𝑋filGen(𝐹 ↾t 𝐴)) = 𝐹) | ||
| Theorem | trfg 23899 | The trace operation and the filGen operation are inverses to one another in some sense, with filGen growing the base set and ↾t shrinking it. See fgtr 23898 for the converse cancellation law. (Contributed by Mario Carneiro, 15-Oct-2015.) |
| ⊢ ((𝐹 ∈ (Fil‘𝐴) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉) → ((𝑋filGen𝐹) ↾t 𝐴) = 𝐹) | ||
| Theorem | trnei 23900 | The trace, over a set 𝐴, of the filter of the neighborhoods of a point 𝑃 is a filter iff 𝑃 belongs to the closure of 𝐴. (This is trfil2 23895 applied to a filter of neighborhoods.) (Contributed by FL, 15-Sep-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
| ⊢ ((𝐽 ∈ (TopOn‘𝑌) ∧ 𝐴 ⊆ 𝑌 ∧ 𝑃 ∈ 𝑌) → (𝑃 ∈ ((cls‘𝐽)‘𝐴) ↔ (((nei‘𝐽)‘{𝑃}) ↾t 𝐴) ∈ (Fil‘𝐴))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |