Home | Metamath
Proof Explorer Theorem List (p. 225 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 | t1hmph 22401 | T1 is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Fre → 𝐾 ∈ Fre)) | ||
Theorem | haushmph 22402 | Hausdorff-ness is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Haus → 𝐾 ∈ Haus)) | ||
Theorem | reghmph 22403 | Regularity is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Reg → 𝐾 ∈ Reg)) | ||
Theorem | nrmhmph 22404 | Normality is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm)) | ||
Theorem | hmph0 22405 | A topology homeomorphic to the empty set is empty. (Contributed by FL, 18-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐽 ≃ {∅} ↔ 𝐽 = {∅}) | ||
Theorem | hmphdis 22406 | Homeomorphisms preserve topological discretion. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ≃ 𝒫 𝐴 → 𝐽 = 𝒫 𝑋) | ||
Theorem | hmphindis 22407 | Homeomorphisms preserve topological indiscretion. (Contributed by FL, 18-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ≃ {∅, 𝐴} → 𝐽 = {∅, 𝑋}) | ||
Theorem | indishmph 22408 | 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 22409 | Homeomorphisms preserve the cardinality of the underlying sets. (Contributed by FL, 17-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ (𝐽 ≃ 𝐾 → 𝑋 ≈ 𝑌) | ||
Theorem | cmphaushmeo 22410 | 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 22411 | Lemma for ordthmeo 22412. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 & ⊢ 𝑌 = dom 𝑆 ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝐹 ∈ ((ordTop‘𝑅) Cn (ordTop‘𝑆))) | ||
Theorem | ordthmeo 22412 | 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 22413* | 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 22414* | Show inverse for the "swap components" operation on a Cartesian product. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 〈𝑥, 𝑦〉) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈𝑦, 𝑥〉)) = ( I ↾ (𝑋 × 𝑌)) | ||
Theorem | txswaphmeo 22415* | There is a homeomorphism from 𝑋 × 𝑌 to 𝑌 × 𝑋. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈𝑦, 𝑥〉) ∈ ((𝐽 ×t 𝐾)Homeo(𝐾 ×t 𝐽))) | ||
Theorem | pt1hmeo 22416* | 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 22417* | 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 22418* | 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 22419* | The function 𝐹 used in xpsval 16845 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 22420 | A binary product of topologies is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) ⇒ ⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝑇 ∈ TopSp) | ||
Theorem | xpstopnlem2 22421* | Lemma for xpstopn 22422. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝐽 = (TopOpen‘𝑅) & ⊢ 𝐾 = (TopOpen‘𝑆) & ⊢ 𝑂 = (TopOpen‘𝑇) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) ⇒ ⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝑂 = (𝐽 ×t 𝐾)) | ||
Theorem | xpstopn 22422 | 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 22423 | 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 22424* | 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 22425* | The Exponential Law for topological spaces. The "currying" function 𝐹 is a homeomorphism on function spaces when 𝐽 and 𝐾 are exponentiable spaces (by xkococn 22270, 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 22426 | 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 22427* | 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 22428* | 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 22429 | 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 22430 | Lemma for ist1-5 22432 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 22431 | 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 22432 | 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 22433 | 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 22434 | 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 22359. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ ((𝐽 ∈ Nrm ∧ 𝐽 ∈ Fre) → 𝐽 ∈ Reg) | ||
Theorem | reghaus 22435 | 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 22436 | 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 22437* | Membership in a one-parameter class of sets. (Contributed by Stefan O'Rear, 28-Jul-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ {𝑦 ∈ 𝐵 ∣ 𝜑}) & ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶) & ⊢ (𝑥 ∈ 𝐷 → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝑌 ∈ (𝐹‘𝑋) ↔ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓)) | ||
Theorem | elmptrab2 22438* | 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 22439* | 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 22440 | There are no empty filter bases. (Contributed by Jeff Hankins, 1-Sep-2009.) (Revised by Mario Carneiro, 28-Jul-2015.) |
⊢ (𝐹 ∈ (fBas‘𝐵) → 𝐹 ≠ ∅) | ||
Theorem | 0nelfb 22441 | No filter base contains the empty set. (Contributed by Jeff Hankins, 1-Sep-2009.) (Revised by Mario Carneiro, 28-Jul-2015.) |
⊢ (𝐹 ∈ (fBas‘𝐵) → ¬ ∅ ∈ 𝐹) | ||
Theorem | fbsspw 22442 | A filter base on a set is a subset of the power set. (Contributed by Stefan O'Rear, 28-Jul-2015.) |
⊢ (𝐹 ∈ (fBas‘𝐵) → 𝐹 ⊆ 𝒫 𝐵) | ||
Theorem | fbelss 22443 | An element of the filter base is a subset of the base set. (Contributed by Stefan O'Rear, 28-Jul-2015.) |
⊢ ((𝐹 ∈ (fBas‘𝐵) ∧ 𝑋 ∈ 𝐹) → 𝑋 ⊆ 𝐵) | ||
Theorem | fbdmn0 22444 | 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 22445* | The predicate "𝐹 is a filter base." (Contributed by Jeff Hankins, 1-Sep-2009.) (Revised by Stefan O'Rear, 28-Jul-2015.) |
⊢ (𝐵 ∈ 𝐴 → (𝐹 ∈ (fBas‘𝐵) ↔ (𝐹 ⊆ 𝒫 𝐵 ∧ (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦))))) | ||
Theorem | fbasssin 22446* | 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 22447* | 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 22448* | 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 22449 | 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 22450* | 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 22451 | 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 22452* | 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 22453 | 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 22454* | 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 22455 | Extend class notation with the set of filters on a set. |
class Fil | ||
Definition | df-fil 22456* | 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 22457* | The predicate "is a filter." (Contributed by FL, 20-Jul-2007.) (Revised by Mario Carneiro, 28-Jul-2015.) |
⊢ (𝐹 ∈ (Fil‘𝑋) ↔ (𝐹 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ 𝒫 𝑋((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝐹))) | ||
Theorem | filfbas 22458 | A filter is a filter base. (Contributed by Jeff Hankins, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Jul-2015.) |
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋)) | ||
Theorem | 0nelfil 22459 | 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 22460 | An element of a filter is nonempty. (Contributed by FL, 24-May-2011.) (Revised by Mario Carneiro, 28-Jul-2015.) |
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → 𝐴 ≠ ∅) | ||
Theorem | filsspw 22461 | A filter is a subset of the power set of the base set. (Contributed by Stefan O'Rear, 28-Jul-2015.) |
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋) | ||
Theorem | filelss 22462 | An element of a filter is a subset of the base set. (Contributed by Stefan O'Rear, 28-Jul-2015.) |
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → 𝐴 ⊆ 𝑋) | ||
Theorem | filss 22463 | A filter is closed under taking supersets. (Contributed by FL, 20-Jul-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.) |
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ⊆ 𝑋 ∧ 𝐴 ⊆ 𝐵)) → 𝐵 ∈ 𝐹) | ||
Theorem | filin 22464 | A filter is closed under taking intersections. (Contributed by FL, 20-Jul-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.) |
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹) → (𝐴 ∩ 𝐵) ∈ 𝐹) | ||
Theorem | filtop 22465 | The underlying set belongs to the filter. (Contributed by FL, 20-Jul-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.) |
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹) | ||
Theorem | isfil2 22466* | 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 22467* | Lemma for isfild 22468. (Contributed by Mario Carneiro, 1-Dec-2013.) |
⊢ (𝜑 → (𝑥 ∈ 𝐹 ↔ (𝑥 ⊆ 𝐴 ∧ 𝜓))) & ⊢ (𝜑 → 𝐴 ∈ V) ⇒ ⊢ (𝜑 → (𝐵 ∈ 𝐹 ↔ (𝐵 ⊆ 𝐴 ∧ [𝐵 / 𝑥]𝜓))) | ||
Theorem | isfild 22468* | 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.) |
⊢ (𝜑 → (𝑥 ∈ 𝐹 ↔ (𝑥 ⊆ 𝐴 ∧ 𝜓))) & ⊢ (𝜑 → 𝐴 ∈ V) & ⊢ (𝜑 → [𝐴 / 𝑥]𝜓) & ⊢ (𝜑 → ¬ [∅ / 𝑥]𝜓) & ⊢ ((𝜑 ∧ 𝑦 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝑦) → ([𝑧 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜓)) & ⊢ ((𝜑 ∧ 𝑦 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝐴) → (([𝑦 / 𝑥]𝜓 ∧ [𝑧 / 𝑥]𝜓) → [(𝑦 ∩ 𝑧) / 𝑥]𝜓)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (Fil‘𝐴)) | ||
Theorem | filfi 22469 | 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 22470 | 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 22471 | 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 22472 | 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 22473 | The intersection of two filters is a filter. Use fiint 8797 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 22474 | 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 22475 | 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 22476 | Condition for a singleton to be a filter base. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐵 ∈ 𝑉) → {𝐴} ∈ (fBas‘𝐵)) | ||
Theorem | fsubbas 22477 | 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 22478 | 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 22479* | 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 22480* | 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 22481* | 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 22482 | 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 22483 | 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 22484* | 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 22485 | A filter generates itself. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑋filGen𝐹) = 𝐹) | ||
Theorem | elfilss 22486* | An element belongs to a filter iff any element below it does. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ 𝐹 ↔ ∃𝑡 ∈ 𝐹 𝑡 ⊆ 𝐴)) | ||
Theorem | filfinnfr 22487 | 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 22488 | 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 22489 | Absorption law for filter generation. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹)) | ||
Theorem | neifil 22490 | 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 22491 | Recover the base set from a filter. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
⊢ (𝐹 ∈ (Fil‘𝑋) → ∪ 𝐹 = 𝑋) | ||
Theorem | filunirn 22492 | Two ways to express a filter on an unspecified base. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
⊢ (𝐹 ∈ ∪ ran Fil ↔ 𝐹 ∈ (Fil‘∪ 𝐹)) | ||
Theorem | filconn 22493 | 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 22494* | 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 22495* | 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 22496 | 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 22497* | 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 22498 | Conditions for the trace of a filter 𝐿 to be a filter. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ¬ (𝑌 ∖ 𝐴) ∈ 𝐿)) | ||
Theorem | trfilss 22499 | 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 22500 | 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 𝐴)) = 𝐹) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |