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