![]() |
Metamath
Proof Explorer Theorem List (p. 239 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hmphtop 23801 | Reverse closure for the homeomorphic predicate. (Contributed by Mario Carneiro, 22-Aug-2015.) |
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Top ∧ 𝐾 ∈ Top)) | ||
Theorem | hmphtop1 23802 | The relation "being homeomorphic to" implies the operands are topologies. (Contributed by FL, 23-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) |
⊢ (𝐽 ≃ 𝐾 → 𝐽 ∈ Top) | ||
Theorem | hmphtop2 23803 | The relation "being homeomorphic to" implies the operands are topologies. (Contributed by FL, 23-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) |
⊢ (𝐽 ≃ 𝐾 → 𝐾 ∈ Top) | ||
Theorem | hmphref 23804 | "Is homeomorphic to" is reflexive. (Contributed by FL, 25-Feb-2007.) (Proof shortened by Mario Carneiro, 23-Aug-2015.) |
⊢ (𝐽 ∈ Top → 𝐽 ≃ 𝐽) | ||
Theorem | hmphsym 23805 | "Is homeomorphic to" is symmetric. (Contributed by FL, 8-Mar-2007.) (Proof shortened by Mario Carneiro, 30-May-2014.) |
⊢ (𝐽 ≃ 𝐾 → 𝐾 ≃ 𝐽) | ||
Theorem | hmphtr 23806 | "Is homeomorphic to" is transitive. (Contributed by FL, 9-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) |
⊢ ((𝐽 ≃ 𝐾 ∧ 𝐾 ≃ 𝐿) → 𝐽 ≃ 𝐿) | ||
Theorem | hmpher 23807 | "Is homeomorphic to" is an equivalence relation. (Contributed by FL, 22-Mar-2007.) (Revised by Mario Carneiro, 23-Aug-2015.) |
⊢ ≃ Er Top | ||
Theorem | hmphen 23808 | Homeomorphisms preserve the cardinality of the topologies. (Contributed by FL, 1-Jun-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐽 ≃ 𝐾 → 𝐽 ≈ 𝐾) | ||
Theorem | hmphsymb 23809 | "Is homeomorphic to" is symmetric. (Contributed by FL, 22-Feb-2007.) |
⊢ (𝐽 ≃ 𝐾 ↔ 𝐾 ≃ 𝐽) | ||
Theorem | haushmphlem 23810* | Lemma for haushmph 23815 and similar theorems. If the topological property 𝐴 is preserved under injective preimages, then property 𝐴 is preserved under homeomorphisms. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ (𝐽 ∈ 𝐴 → 𝐽 ∈ Top) & ⊢ ((𝐽 ∈ 𝐴 ∧ 𝑓:∪ 𝐾–1-1→∪ 𝐽 ∧ 𝑓 ∈ (𝐾 Cn 𝐽)) → 𝐾 ∈ 𝐴) ⇒ ⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ 𝐴 → 𝐾 ∈ 𝐴)) | ||
Theorem | cmphmph 23811 | Compactness is a topological property-that is, for any two homeomorphic topologies, either both are compact or neither is. (Contributed by Jeff Hankins, 30-Jun-2009.) (Revised by Mario Carneiro, 23-Aug-2015.) |
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Comp → 𝐾 ∈ Comp)) | ||
Theorem | connhmph 23812 | Connectedness is a topological property. (Contributed by Jeff Hankins, 3-Jul-2009.) |
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Conn → 𝐾 ∈ Conn)) | ||
Theorem | t0hmph 23813 | T0 is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Kol2 → 𝐾 ∈ Kol2)) | ||
Theorem | t1hmph 23814 | T1 is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Fre → 𝐾 ∈ Fre)) | ||
Theorem | haushmph 23815 | Hausdorff-ness is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Haus → 𝐾 ∈ Haus)) | ||
Theorem | reghmph 23816 | Regularity is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Reg → 𝐾 ∈ Reg)) | ||
Theorem | nrmhmph 23817 | Normality is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ (𝐽 ≃ 𝐾 → (𝐽 ∈ Nrm → 𝐾 ∈ Nrm)) | ||
Theorem | hmph0 23818 | A topology homeomorphic to the empty set is empty. (Contributed by FL, 18-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐽 ≃ {∅} ↔ 𝐽 = {∅}) | ||
Theorem | hmphdis 23819 | Homeomorphisms preserve topological discreteness. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ≃ 𝒫 𝐴 → 𝐽 = 𝒫 𝑋) | ||
Theorem | hmphindis 23820 | Homeomorphisms preserve topological indiscreteness. (Contributed by FL, 18-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ≃ {∅, 𝐴} → 𝐽 = {∅, 𝑋}) | ||
Theorem | indishmph 23821 | 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 23822 | Homeomorphisms preserve the cardinality of the underlying sets. (Contributed by FL, 17-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝑌 = ∪ 𝐾 ⇒ ⊢ (𝐽 ≃ 𝐾 → 𝑋 ≈ 𝑌) | ||
Theorem | cmphaushmeo 23823 | 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 23824 | Lemma for ordthmeo 23825. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 & ⊢ 𝑌 = dom 𝑆 ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ∧ 𝐹 Isom 𝑅, 𝑆 (𝑋, 𝑌)) → 𝐹 ∈ ((ordTop‘𝑅) Cn (ordTop‘𝑆))) | ||
Theorem | ordthmeo 23825 | 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 23826* | 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 23827* | Show inverse for the "swap components" operation on a Cartesian product. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝑦 ∈ 𝑌, 𝑥 ∈ 𝑋 ↦ 〈𝑥, 𝑦〉) ∘ (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈𝑦, 𝑥〉)) = ( I ↾ (𝑋 × 𝑌)) | ||
Theorem | txswaphmeo 23828* | There is a homeomorphism from 𝑋 × 𝑌 to 𝑌 × 𝑋. (Contributed by Mario Carneiro, 21-Mar-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 〈𝑦, 𝑥〉) ∈ ((𝐽 ×t 𝐾)Homeo(𝐾 ×t 𝐽))) | ||
Theorem | pt1hmeo 23829* | 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 23830* | 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 23831* | 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 23832* | The function 𝐹 used in xpsval 17616 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 23833 | A binary product of topologies is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) ⇒ ⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝑇 ∈ TopSp) | ||
Theorem | xpstopnlem2 23834* | Lemma for xpstopn 23835. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) & ⊢ 𝐽 = (TopOpen‘𝑅) & ⊢ 𝐾 = (TopOpen‘𝑆) & ⊢ 𝑂 = (TopOpen‘𝑇) & ⊢ 𝑋 = (Base‘𝑅) & ⊢ 𝑌 = (Base‘𝑆) & ⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ {〈∅, 𝑥〉, 〈1o, 𝑦〉}) ⇒ ⊢ ((𝑅 ∈ TopSp ∧ 𝑆 ∈ TopSp) → 𝑂 = (𝐽 ×t 𝐾)) | ||
Theorem | xpstopn 23835 | 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 23836 | 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 23837* | 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 23838* | The Exponential Law for topological spaces. The "currying" function 𝐹 is a homeomorphism on function spaces when 𝐽 and 𝐾 are exponentiable spaces (by xkococn 23683, 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 23839 | 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 23840* | 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 23841* | 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 23842 | 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 23843 | Lemma for ist1-5 23845 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 23844 | 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 23845 | 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 23846 | 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 23847 | 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 23772. (Contributed by Mario Carneiro, 25-Aug-2015.) |
⊢ ((𝐽 ∈ Nrm ∧ 𝐽 ∈ Fre) → 𝐽 ∈ Reg) | ||
Theorem | reghaus 23848 | 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 23849 | 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 23850* | Membership in a one-parameter class of sets. (Contributed by Stefan O'Rear, 28-Jul-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ {𝑦 ∈ 𝐵 ∣ 𝜑}) & ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶) & ⊢ (𝑥 ∈ 𝐷 → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝑌 ∈ (𝐹‘𝑋) ↔ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓)) | ||
Theorem | elmptrab2 23851* | 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 23852* | 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 23853 | There are no empty filter bases. (Contributed by Jeff Hankins, 1-Sep-2009.) (Revised by Mario Carneiro, 28-Jul-2015.) |
⊢ (𝐹 ∈ (fBas‘𝐵) → 𝐹 ≠ ∅) | ||
Theorem | 0nelfb 23854 | No filter base contains the empty set. (Contributed by Jeff Hankins, 1-Sep-2009.) (Revised by Mario Carneiro, 28-Jul-2015.) |
⊢ (𝐹 ∈ (fBas‘𝐵) → ¬ ∅ ∈ 𝐹) | ||
Theorem | fbsspw 23855 | A filter base on a set is a subset of the power set. (Contributed by Stefan O'Rear, 28-Jul-2015.) |
⊢ (𝐹 ∈ (fBas‘𝐵) → 𝐹 ⊆ 𝒫 𝐵) | ||
Theorem | fbelss 23856 | An element of the filter base is a subset of the base set. (Contributed by Stefan O'Rear, 28-Jul-2015.) |
⊢ ((𝐹 ∈ (fBas‘𝐵) ∧ 𝑋 ∈ 𝐹) → 𝑋 ⊆ 𝐵) | ||
Theorem | fbdmn0 23857 | 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 23858* | The predicate "𝐹 is a filter base." (Contributed by Jeff Hankins, 1-Sep-2009.) (Revised by Stefan O'Rear, 28-Jul-2015.) |
⊢ (𝐵 ∈ 𝐴 → (𝐹 ∈ (fBas‘𝐵) ↔ (𝐹 ⊆ 𝒫 𝐵 ∧ (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦))))) | ||
Theorem | fbasssin 23859* | 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 23860* | 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 23861* | 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 23862 | 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 23863* | 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 23864 | 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 23865* | 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 23866 | 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 23867* | 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 23868 | Extend class notation with the set of filters on a set. |
class Fil | ||
Definition | df-fil 23869* | 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 23870* | The predicate "is a filter." (Contributed by FL, 20-Jul-2007.) (Revised by Mario Carneiro, 28-Jul-2015.) |
⊢ (𝐹 ∈ (Fil‘𝑋) ↔ (𝐹 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ 𝒫 𝑋((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝐹))) | ||
Theorem | filfbas 23871 | A filter is a filter base. (Contributed by Jeff Hankins, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Jul-2015.) |
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (fBas‘𝑋)) | ||
Theorem | 0nelfil 23872 | 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 23873 | An element of a filter is nonempty. (Contributed by FL, 24-May-2011.) (Revised by Mario Carneiro, 28-Jul-2015.) |
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → 𝐴 ≠ ∅) | ||
Theorem | filsspw 23874 | A filter is a subset of the power set of the base set. (Contributed by Stefan O'Rear, 28-Jul-2015.) |
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋) | ||
Theorem | filelss 23875 | An element of a filter is a subset of the base set. (Contributed by Stefan O'Rear, 28-Jul-2015.) |
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹) → 𝐴 ⊆ 𝑋) | ||
Theorem | filss 23876 | A filter is closed under taking supersets. (Contributed by FL, 20-Jul-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.) |
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ⊆ 𝑋 ∧ 𝐴 ⊆ 𝐵)) → 𝐵 ∈ 𝐹) | ||
Theorem | filin 23877 | A filter is closed under taking intersections. (Contributed by FL, 20-Jul-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.) |
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹) → (𝐴 ∩ 𝐵) ∈ 𝐹) | ||
Theorem | filtop 23878 | The underlying set belongs to the filter. (Contributed by FL, 20-Jul-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.) |
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹) | ||
Theorem | isfil2 23879* | 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 23880* | Lemma for isfild 23881. (Contributed by Mario Carneiro, 1-Dec-2013.) |
⊢ (𝜑 → (𝑥 ∈ 𝐹 ↔ (𝑥 ⊆ 𝐴 ∧ 𝜓))) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐵 ∈ 𝐹 ↔ (𝐵 ⊆ 𝐴 ∧ [𝐵 / 𝑥]𝜓))) | ||
Theorem | isfild 23881* | 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 23882 | 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 23883 | 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 23884 | 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 23885 | 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 23886 | The intersection of two filters is a filter. Use fiint 9363 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 23887 | 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 23888 | 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 23889 | Condition for a singleton to be a filter base. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐵 ∈ 𝑉) → {𝐴} ∈ (fBas‘𝐵)) | ||
Theorem | fsubbas 23890 | 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 23891 | 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 23892* | 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 23893* | 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 23894* | 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 23895 | 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 23896 | 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 23897* | 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 23898 | A filter generates itself. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑋filGen𝐹) = 𝐹) | ||
Theorem | elfilss 23899* | An element belongs to a filter iff any element below it does. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ 𝐹 ↔ ∃𝑡 ∈ 𝐹 𝑡 ⊆ 𝐴)) | ||
Theorem | filfinnfr 23900 | 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) → ∩ 𝐹 ≠ ∅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |