![]() |
Metamath
Proof Explorer Theorem List (p. 234 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hmphindis 23301 | Homeomorphisms preserve topological indiscreteness. (Contributed by FL, 18-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
β’ π = βͺ π½ β β’ (π½ β {β , π΄} β π½ = {β , π}) | ||
Theorem | indishmph 23302 | 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 23303 | Homeomorphisms preserve the cardinality of the underlying sets. (Contributed by FL, 17-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ (π½ β πΎ β π β π) | ||
Theorem | cmphaushmeo 23304 | 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 23305 | Lemma for ordthmeo 23306. (Contributed by Mario Carneiro, 9-Sep-2015.) |
β’ π = dom π & β’ π = dom π β β’ ((π β π β§ π β π β§ πΉ Isom π , π (π, π)) β πΉ β ((ordTopβπ ) Cn (ordTopβπ))) | ||
Theorem | ordthmeo 23306 | 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 23307* | 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 23308* | Show inverse for the "swap components" operation on a Cartesian product. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ ((π¦ β π, π₯ β π β¦ β¨π₯, π¦β©) β (π₯ β π, π¦ β π β¦ β¨π¦, π₯β©)) = ( I βΎ (π Γ π)) | ||
Theorem | txswaphmeo 23309* | There is a homeomorphism from π Γ π to π Γ π. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π₯ β π, π¦ β π β¦ β¨π¦, π₯β©) β ((π½ Γt πΎ)Homeo(πΎ Γt π½))) | ||
Theorem | pt1hmeo 23310* | 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 23311* | 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 23312* | 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 23313* | The function πΉ used in xpsval 17516 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 23314 | A binary product of topologies is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ π = (π Γs π) β β’ ((π β TopSp β§ π β TopSp) β π β TopSp) | ||
Theorem | xpstopnlem2 23315* | Lemma for xpstopn 23316. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ π = (π Γs π) & β’ π½ = (TopOpenβπ ) & β’ πΎ = (TopOpenβπ) & β’ π = (TopOpenβπ) & β’ π = (Baseβπ ) & β’ π = (Baseβπ) & β’ πΉ = (π₯ β π, π¦ β π β¦ {β¨β , π₯β©, β¨1o, π¦β©}) β β’ ((π β TopSp β§ π β TopSp) β π = (π½ Γt πΎ)) | ||
Theorem | xpstopn 23316 | 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 23317 | 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 23318* | 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 23319* | The Exponential Law for topological spaces. The "currying" function πΉ is a homeomorphism on function spaces when π½ and πΎ are exponentiable spaces (by xkococn 23164, 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 23320 | 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 23321* | 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 23322* | 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 23323 | 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 23324 | Lemma for ist1-5 23326 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 23325 | 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 23326 | 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 23327 | 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 23328 | 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 23253. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ ((π½ β Nrm β§ π½ β Fre) β π½ β Reg) | ||
Theorem | reghaus 23329 | 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 23330 | 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 23331* | Membership in a one-parameter class of sets. (Contributed by Stefan O'Rear, 28-Jul-2015.) |
β’ πΉ = (π₯ β π· β¦ {π¦ β π΅ β£ π}) & β’ ((π₯ = π β§ π¦ = π) β (π β π)) & β’ (π₯ = π β π΅ = πΆ) & β’ (π₯ β π· β π΅ β π) β β’ (π β (πΉβπ) β (π β π· β§ π β πΆ β§ π)) | ||
Theorem | elmptrab2 23332* | 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 23333* | 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 23334 | There are no empty filter bases. (Contributed by Jeff Hankins, 1-Sep-2009.) (Revised by Mario Carneiro, 28-Jul-2015.) |
β’ (πΉ β (fBasβπ΅) β πΉ β β ) | ||
Theorem | 0nelfb 23335 | No filter base contains the empty set. (Contributed by Jeff Hankins, 1-Sep-2009.) (Revised by Mario Carneiro, 28-Jul-2015.) |
β’ (πΉ β (fBasβπ΅) β Β¬ β β πΉ) | ||
Theorem | fbsspw 23336 | A filter base on a set is a subset of the power set. (Contributed by Stefan O'Rear, 28-Jul-2015.) |
β’ (πΉ β (fBasβπ΅) β πΉ β π« π΅) | ||
Theorem | fbelss 23337 | An element of the filter base is a subset of the base set. (Contributed by Stefan O'Rear, 28-Jul-2015.) |
β’ ((πΉ β (fBasβπ΅) β§ π β πΉ) β π β π΅) | ||
Theorem | fbdmn0 23338 | 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 23339* | The predicate "πΉ is a filter base." (Contributed by Jeff Hankins, 1-Sep-2009.) (Revised by Stefan O'Rear, 28-Jul-2015.) |
β’ (π΅ β π΄ β (πΉ β (fBasβπ΅) β (πΉ β π« π΅ β§ (πΉ β β β§ β β πΉ β§ βπ₯ β πΉ βπ¦ β πΉ βπ§ β πΉ π§ β (π₯ β© π¦))))) | ||
Theorem | fbasssin 23340* | 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 23341* | 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 23342* | 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 23343 | 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 23344* | 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 23345 | 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 23346* | 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 23347 | 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 23348* | 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 23349 | Extend class notation with the set of filters on a set. |
class Fil | ||
Definition | df-fil 23350* | 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 23351* | The predicate "is a filter." (Contributed by FL, 20-Jul-2007.) (Revised by Mario Carneiro, 28-Jul-2015.) |
β’ (πΉ β (Filβπ) β (πΉ β (fBasβπ) β§ βπ₯ β π« π((πΉ β© π« π₯) β β β π₯ β πΉ))) | ||
Theorem | filfbas 23352 | A filter is a filter base. (Contributed by Jeff Hankins, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Jul-2015.) |
β’ (πΉ β (Filβπ) β πΉ β (fBasβπ)) | ||
Theorem | 0nelfil 23353 | 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 23354 | An element of a filter is nonempty. (Contributed by FL, 24-May-2011.) (Revised by Mario Carneiro, 28-Jul-2015.) |
β’ ((πΉ β (Filβπ) β§ π΄ β πΉ) β π΄ β β ) | ||
Theorem | filsspw 23355 | A filter is a subset of the power set of the base set. (Contributed by Stefan O'Rear, 28-Jul-2015.) |
β’ (πΉ β (Filβπ) β πΉ β π« π) | ||
Theorem | filelss 23356 | An element of a filter is a subset of the base set. (Contributed by Stefan O'Rear, 28-Jul-2015.) |
β’ ((πΉ β (Filβπ) β§ π΄ β πΉ) β π΄ β π) | ||
Theorem | filss 23357 | A filter is closed under taking supersets. (Contributed by FL, 20-Jul-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.) |
β’ ((πΉ β (Filβπ) β§ (π΄ β πΉ β§ π΅ β π β§ π΄ β π΅)) β π΅ β πΉ) | ||
Theorem | filin 23358 | A filter is closed under taking intersections. (Contributed by FL, 20-Jul-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.) |
β’ ((πΉ β (Filβπ) β§ π΄ β πΉ β§ π΅ β πΉ) β (π΄ β© π΅) β πΉ) | ||
Theorem | filtop 23359 | The underlying set belongs to the filter. (Contributed by FL, 20-Jul-2007.) (Revised by Stefan O'Rear, 28-Jul-2015.) |
β’ (πΉ β (Filβπ) β π β πΉ) | ||
Theorem | isfil2 23360* | 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 23361* | Lemma for isfild 23362. (Contributed by Mario Carneiro, 1-Dec-2013.) |
β’ (π β (π₯ β πΉ β (π₯ β π΄ β§ π))) & β’ (π β π΄ β π) β β’ (π β (π΅ β πΉ β (π΅ β π΄ β§ [π΅ / π₯]π))) | ||
Theorem | isfild 23362* | 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 23363 | 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 23364 | 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 23365 | 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 23366 | 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 23367 | The intersection of two filters is a filter. Use fiint 9324 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 23368 | 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 23369 | 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 23370 | Condition for a singleton to be a filter base. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
β’ ((π΄ β π΅ β§ π΄ β β β§ π΅ β π) β {π΄} β (fBasβπ΅)) | ||
Theorem | fsubbas 23371 | 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 23372 | 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 23373* | 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 23374* | 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 23375* | 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 23376 | 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 23377 | 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 23378* | 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 23379 | A filter generates itself. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
β’ (πΉ β (Filβπ) β (πfilGenπΉ) = πΉ) | ||
Theorem | elfilss 23380* | An element belongs to a filter iff any element below it does. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
β’ ((πΉ β (Filβπ) β§ π΄ β π) β (π΄ β πΉ β βπ‘ β πΉ π‘ β π΄)) | ||
Theorem | filfinnfr 23381 | 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 23382 | 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 23383 | Absorption law for filter generation. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ ((πΉ β (fBasβπ) β§ π β π) β (πfilGen(πfilGenπΉ)) = (πfilGenπΉ)) | ||
Theorem | neifil 23384 | 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 23385 | Recover the base set from a filter. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
β’ (πΉ β (Filβπ) β βͺ πΉ = π) | ||
Theorem | filunirn 23386 | Two ways to express a filter on an unspecified base. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
β’ (πΉ β βͺ ran Fil β πΉ β (Filββͺ πΉ)) | ||
Theorem | filconn 23387 | 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 23388* | 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 23389* | 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 23390 | 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 23391* | 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 23392 | Conditions for the trace of a filter πΏ to be a filter. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
β’ ((πΏ β (Filβπ) β§ π΄ β π) β ((πΏ βΎt π΄) β (Filβπ΄) β Β¬ (π β π΄) β πΏ)) | ||
Theorem | trfilss 23393 | 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 23394 | 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 23395 | 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 23394 for the converse cancellation law. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ ((πΉ β (Filβπ΄) β§ π΄ β π β§ π β π) β ((πfilGenπΉ) βΎt π΄) = πΉ) | ||
Theorem | trnei 23396 | 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 23391 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 23397* | 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 23398* | 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 23399* | 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βπ΄)) | ||
Theorem | zfbas 23400 | The set of upper sets of integers is a filter base on β€, which corresponds to convergence of sequences on β€. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ ran β€β₯ β (fBasββ€) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |