![]() |
Metamath
Proof Explorer Theorem List (p. 235 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 | uzrest 23401 | The restriction of the set of upper sets of integers to an upper set of integers is the set of upper sets of integers based at a point above the cutoff. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ π = (β€β₯βπ) β β’ (π β β€ β (ran β€β₯ βΎt π) = (β€β₯ β π)) | ||
Theorem | uzfbas 23402 | The set of upper sets of integers based at a point in a fixed upper integer set like β is a filter base on β, which corresponds to convergence of sequences on β. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ π = (β€β₯βπ) β β’ (π β β€ β (β€β₯ β π) β (fBasβπ)) | ||
Syntax | cufil 23403 | Extend class notation with the ultrafilters-on-a-set function. |
class UFil | ||
Syntax | cufl 23404 | Extend class notation with the ultrafilter lemma. |
class UFL | ||
Definition | df-ufil 23405* | Define the set of ultrafilters on a set. An ultrafilter is a filter that gives a definite result for every subset. (Contributed by Jeff Hankins, 30-Nov-2009.) |
β’ UFil = (π β V β¦ {π β (Filβπ) β£ βπ₯ β π« π(π₯ β π β¨ (π β π₯) β π)}) | ||
Definition | df-ufl 23406* | Define the class of base sets for which the ultrafilter lemma filssufil 23416 holds. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ UFL = {π₯ β£ βπ β (Filβπ₯)βπ β (UFilβπ₯)π β π} | ||
Theorem | isufil 23407* | The property of being an ultrafilter. (Contributed by Jeff Hankins, 30-Nov-2009.) (Revised by Mario Carneiro, 29-Jul-2015.) |
β’ (πΉ β (UFilβπ) β (πΉ β (Filβπ) β§ βπ₯ β π« π(π₯ β πΉ β¨ (π β π₯) β πΉ))) | ||
Theorem | ufilfil 23408 | An ultrafilter is a filter. (Contributed by Jeff Hankins, 1-Dec-2009.) (Revised by Mario Carneiro, 29-Jul-2015.) |
β’ (πΉ β (UFilβπ) β πΉ β (Filβπ)) | ||
Theorem | ufilss 23409 | For any subset of the base set of an ultrafilter, either the set is in the ultrafilter or the complement is. (Contributed by Jeff Hankins, 1-Dec-2009.) (Revised by Mario Carneiro, 29-Jul-2015.) |
β’ ((πΉ β (UFilβπ) β§ π β π) β (π β πΉ β¨ (π β π) β πΉ)) | ||
Theorem | ufilb 23410 | The complement is in an ultrafilter iff the set is not. (Contributed by Mario Carneiro, 11-Dec-2013.) (Revised by Mario Carneiro, 29-Jul-2015.) |
β’ ((πΉ β (UFilβπ) β§ π β π) β (Β¬ π β πΉ β (π β π) β πΉ)) | ||
Theorem | ufilmax 23411 | Any filter finer than an ultrafilter is actually equal to it. (Contributed by Jeff Hankins, 1-Dec-2009.) (Revised by Mario Carneiro, 29-Jul-2015.) |
β’ ((πΉ β (UFilβπ) β§ πΊ β (Filβπ) β§ πΉ β πΊ) β πΉ = πΊ) | ||
Theorem | isufil2 23412* | The maximal property of an ultrafilter. (Contributed by Jeff Hankins, 30-Nov-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
β’ (πΉ β (UFilβπ) β (πΉ β (Filβπ) β§ βπ β (Filβπ)(πΉ β π β πΉ = π))) | ||
Theorem | ufprim 23413 | An ultrafilter is a prime filter. (Contributed by Jeff Hankins, 1-Jan-2010.) (Revised by Mario Carneiro, 2-Aug-2015.) |
β’ ((πΉ β (UFilβπ) β§ π΄ β π β§ π΅ β π) β ((π΄ β πΉ β¨ π΅ β πΉ) β (π΄ βͺ π΅) β πΉ)) | ||
Theorem | trufil 23414 | Conditions for the trace of an ultrafilter πΏ to be an ultrafilter. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ ((πΏ β (UFilβπ) β§ π΄ β π) β ((πΏ βΎt π΄) β (UFilβπ΄) β π΄ β πΏ)) | ||
Theorem | filssufilg 23415* | A filter is contained in some ultrafilter. This version of filssufil 23416 contains the choice as a hypothesis (in the assumption that π« π« π is well-orderable). (Contributed by Mario Carneiro, 24-May-2015.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
β’ ((πΉ β (Filβπ) β§ π« π« π β dom card) β βπ β (UFilβπ)πΉ β π) | ||
Theorem | filssufil 23416* | A filter is contained in some ultrafilter. (Requires the Axiom of Choice, via numth3 10465.) (Contributed by Jeff Hankins, 2-Dec-2009.) (Revised by Stefan O'Rear, 29-Jul-2015.) |
β’ (πΉ β (Filβπ) β βπ β (UFilβπ)πΉ β π) | ||
Theorem | isufl 23417* | Define the (strong) ultrafilter lemma, parameterized over base sets. A set π satisfies the ultrafilter lemma if every filter on π is a subset of some ultrafilter. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π β π β (π β UFL β βπ β (Filβπ)βπ β (UFilβπ)π β π)) | ||
Theorem | ufli 23418* | Property of a set that satisfies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((π β UFL β§ πΉ β (Filβπ)) β βπ β (UFilβπ)πΉ β π) | ||
Theorem | numufl 23419 | Consequence of filssufilg 23415: a set whose double powerset is well-orderable satisfies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π« π« π β dom card β π β UFL) | ||
Theorem | fiufl 23420 | A finite set satisfies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π β Fin β π β UFL) | ||
Theorem | acufl 23421 | The axiom of choice implies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (CHOICE β UFL = V) | ||
Theorem | ssufl 23422 | If π is a subset of π and filters extend to ultrafilters in π, then they still do in π. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((π β UFL β§ π β π) β π β UFL) | ||
Theorem | ufileu 23423* | If the ultrafilter containing a given filter is unique, the filter is an ultrafilter. (Contributed by Jeff Hankins, 3-Dec-2009.) (Revised by Mario Carneiro, 2-Oct-2015.) |
β’ (πΉ β (Filβπ) β (πΉ β (UFilβπ) β β!π β (UFilβπ)πΉ β π)) | ||
Theorem | filufint 23424* | A filter is equal to the intersection of the ultrafilters containing it. (Contributed by Jeff Hankins, 1-Jan-2010.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
β’ (πΉ β (Filβπ) β β© {π β (UFilβπ) β£ πΉ β π} = πΉ) | ||
Theorem | uffix 23425* | Lemma for fixufil 23426 and uffixfr 23427. (Contributed by Mario Carneiro, 12-Dec-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
β’ ((π β π β§ π΄ β π) β ({{π΄}} β (fBasβπ) β§ {π₯ β π« π β£ π΄ β π₯} = (πfilGen{{π΄}}))) | ||
Theorem | fixufil 23426* | The condition describing a fixed ultrafilter always produces an ultrafilter. (Contributed by Jeff Hankins, 9-Dec-2009.) (Revised by Mario Carneiro, 12-Dec-2013.) (Revised by Stefan O'Rear, 29-Jul-2015.) |
β’ ((π β π β§ π΄ β π) β {π₯ β π« π β£ π΄ β π₯} β (UFilβπ)) | ||
Theorem | uffixfr 23427* | An ultrafilter is either fixed or free. A fixed ultrafilter is called principal (generated by a single element π΄), and a free ultrafilter is called nonprincipal (having empty intersection). Note that examples of free ultrafilters cannot be defined in ZFC without some form of global choice. (Contributed by Jeff Hankins, 4-Dec-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
β’ (πΉ β (UFilβπ) β (π΄ β β© πΉ β πΉ = {π₯ β π« π β£ π΄ β π₯})) | ||
Theorem | uffix2 23428* | A classification of fixed ultrafilters. (Contributed by Mario Carneiro, 24-May-2015.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
β’ (πΉ β (UFilβπ) β (β© πΉ β β β βπ₯ β π πΉ = {π¦ β π« π β£ π₯ β π¦})) | ||
Theorem | uffixsn 23429 | The singleton of the generator of a fixed ultrafilter is in the filter. (Contributed by Mario Carneiro, 24-May-2015.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
β’ ((πΉ β (UFilβπ) β§ π΄ β β© πΉ) β {π΄} β πΉ) | ||
Theorem | ufildom1 23430 | An ultrafilter is generated by at most one element (because free ultrafilters have no generators and fixed ultrafilters have exactly one). (Contributed by Mario Carneiro, 24-May-2015.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
β’ (πΉ β (UFilβπ) β β© πΉ βΌ 1o) | ||
Theorem | uffinfix 23431* | An ultrafilter containing a finite element is fixed. (Contributed by Jeff Hankins, 5-Dec-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
β’ ((πΉ β (UFilβπ) β§ π β πΉ β§ π β Fin) β βπ₯ β π πΉ = {π¦ β π« π β£ π₯ β π¦}) | ||
Theorem | cfinufil 23432* | An ultrafilter is free iff it contains the FrΓ©chet filter cfinfil 23397 as a subset. (Contributed by NM, 14-Jul-2008.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
β’ (πΉ β (UFilβπ) β (β© πΉ = β β {π₯ β π« π β£ (π β π₯) β Fin} β πΉ)) | ||
Theorem | ufinffr 23433* | An infinite subset is contained in a free ultrafilter. (Contributed by Jeff Hankins, 6-Dec-2009.) (Revised by Mario Carneiro, 4-Dec-2013.) |
β’ ((π β π΅ β§ π΄ β π β§ Ο βΌ π΄) β βπ β (UFilβπ)(π΄ β π β§ β© π = β )) | ||
Theorem | ufilen 23434* | Any infinite set has an ultrafilter on it whose elements are of the same cardinality as the set. Any such ultrafilter is necessarily free. (Contributed by Jeff Hankins, 7-Dec-2009.) (Revised by Stefan O'Rear, 3-Aug-2015.) |
β’ (Ο βΌ π β βπ β (UFilβπ)βπ₯ β π π₯ β π) | ||
Theorem | ufildr 23435 | An ultrafilter gives rise to a connected door topology. (Contributed by Jeff Hankins, 6-Dec-2009.) (Revised by Stefan O'Rear, 3-Aug-2015.) |
β’ π½ = (πΉ βͺ {β }) β β’ (πΉ β (UFilβπ) β (π½ βͺ (Clsdβπ½)) = π« π) | ||
Theorem | fin1aufil 23436 | There are no definable free ultrafilters in ZFC. However, there are free ultrafilters in some choice-denying constructions. Here we show that given an amorphous set (a.k.a. a Ia-finite I-infinite set) π, the set of infinite subsets of π is a free ultrafilter on π. (Contributed by Mario Carneiro, 20-May-2015.) |
β’ πΉ = (π« π β Fin) β β’ (π β (FinIa β Fin) β (πΉ β (UFilβπ) β§ β© πΉ = β )) | ||
Syntax | cfm 23437 | Extend class definition to include the neighborhood filter mapping function. |
class FilMap | ||
Syntax | cflim 23438 | Extend class notation with a function returning the limit of a filter. |
class fLim | ||
Syntax | cflf 23439 | Extend class definition to include the function for filter-based function limits. |
class fLimf | ||
Syntax | cfcls 23440 | Extend class definition to include the cluster point function on filters. |
class fClus | ||
Syntax | cfcf 23441 | Extend class definition to include the function for cluster points of a function. |
class fClusf | ||
Definition | df-fm 23442* | Define a function that takes a filter to a neighborhood filter of the range. (Since we now allow filter bases to have support smaller than the base set, the function has to come first to ensure that curryings are sets.) (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Stefan O'Rear, 20-Jul-2015.) |
β’ FilMap = (π₯ β V, π β V β¦ (π¦ β (fBasβdom π) β¦ (π₯filGenran (π‘ β π¦ β¦ (π β π‘))))) | ||
Definition | df-flim 23443* | Define a function (indexed by a topology π) whose value is the limits of a filter π. (Contributed by Jeff Hankins, 4-Sep-2009.) |
β’ fLim = (π β Top, π β βͺ ran Fil β¦ {π₯ β βͺ π β£ (((neiβπ)β{π₯}) β π β§ π β π« βͺ π)}) | ||
Definition | df-flf 23444* | Define a function that gives the limits of a function π in the filter sense. (Contributed by Jeff Hankins, 14-Oct-2009.) |
β’ fLimf = (π₯ β Top, π¦ β βͺ ran Fil β¦ (π β (βͺ π₯ βm βͺ π¦) β¦ (π₯ fLim ((βͺ π₯ FilMap π)βπ¦)))) | ||
Definition | df-fcls 23445* | Define a function that takes a filter in a topology to its set of cluster points. (Contributed by Jeff Hankins, 10-Nov-2009.) |
β’ fClus = (π β Top, π β βͺ ran Fil β¦ if(βͺ π = βͺ π, β© π₯ β π ((clsβπ)βπ₯), β )) | ||
Definition | df-fcf 23446* | Define a function that gives the cluster points of a function. (Contributed by Jeff Hankins, 24-Nov-2009.) |
β’ fClusf = (π β Top, π β βͺ ran Fil β¦ (π β (βͺ π βm βͺ π) β¦ (π fClus ((βͺ π FilMap π)βπ)))) | ||
Theorem | fmval 23447* | Introduce a function that takes a function from a filtered domain to a set and produces a filter which consists of supersets of images of filter elements. The functions which are dealt with by this function are similar to nets in topology. For example, suppose we have a sequence filtered by the filter generated by its tails under the usual positive integer ordering. Then the elements of this filter are precisely the supersets of tails of this sequence. Under this definition, it is not too difficult to see that the limit of a function in the filter sense captures the notion of convergence of a sequence. As a result, the notion of a filter generalizes many ideas associated with sequences, and this function is one way to make that relationship precise in Metamath. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ ((π β π΄ β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β ((π FilMap πΉ)βπ΅) = (πfilGenran (π¦ β π΅ β¦ (πΉ β π¦)))) | ||
Theorem | fmfil 23448 | A mapping filter is a filter. (Contributed by Jeff Hankins, 18-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ ((π β π΄ β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β ((π FilMap πΉ)βπ΅) β (Filβπ)) | ||
Theorem | fmf 23449 | Pushing-forward via a function induces a mapping on filters. (Contributed by Stefan O'Rear, 8-Aug-2015.) |
β’ ((π β π΄ β§ π β π΅ β§ πΉ:πβΆπ) β (π FilMap πΉ):(fBasβπ)βΆ(Filβπ)) | ||
Theorem | fmss 23450 | A finer filter produces a finer image filter. (Contributed by Jeff Hankins, 16-Nov-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ (((π β π΄ β§ π΅ β (fBasβπ) β§ πΆ β (fBasβπ)) β§ (πΉ:πβΆπ β§ π΅ β πΆ)) β ((π FilMap πΉ)βπ΅) β ((π FilMap πΉ)βπΆ)) | ||
Theorem | elfm 23451* | An element of a mapping filter. (Contributed by Jeff Hankins, 8-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ ((π β πΆ β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (π΄ β ((π FilMap πΉ)βπ΅) β (π΄ β π β§ βπ₯ β π΅ (πΉ β π₯) β π΄))) | ||
Theorem | elfm2 23452* | An element of a mapping filter. (Contributed by Jeff Hankins, 26-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ πΏ = (πfilGenπ΅) β β’ ((π β πΆ β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (π΄ β ((π FilMap πΉ)βπ΅) β (π΄ β π β§ βπ₯ β πΏ (πΉ β π₯) β π΄))) | ||
Theorem | fmfg 23453 | The image filter of a filter base is the same as the image filter of its generated filter. (Contributed by Jeff Hankins, 18-Nov-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ πΏ = (πfilGenπ΅) β β’ ((π β πΆ β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β ((π FilMap πΉ)βπ΅) = ((π FilMap πΉ)βπΏ)) | ||
Theorem | elfm3 23454* | An alternate formulation of elementhood in a mapping filter that requires πΉ to be onto. (Contributed by Jeff Hankins, 1-Oct-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ πΏ = (πfilGenπ΅) β β’ ((π΅ β (fBasβπ) β§ πΉ:πβontoβπ) β (π΄ β ((π FilMap πΉ)βπ΅) β βπ₯ β πΏ π΄ = (πΉ β π₯))) | ||
Theorem | imaelfm 23455 | An image of a filter element is in the image filter. (Contributed by Jeff Hankins, 5-Oct-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ πΏ = (πfilGenπ΅) β β’ (((π β π΄ β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β§ π β πΏ) β (πΉ β π) β ((π FilMap πΉ)βπ΅)) | ||
Theorem | rnelfmlem 23456* | Lemma for rnelfm 23457. (Contributed by Jeff Hankins, 14-Nov-2009.) |
β’ (((π β π΄ β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ ran πΉ β πΏ) β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β (fBasβπ)) | ||
Theorem | rnelfm 23457 | A condition for a filter to be an image filter for a given function. (Contributed by Jeff Hankins, 14-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ ((π β π΄ β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β (πΏ β ran (π FilMap πΉ) β ran πΉ β πΏ)) | ||
Theorem | fmfnfmlem1 23458* | Lemma for fmfnfm 23462. (Contributed by Jeff Hankins, 18-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ (π β π΅ β (fBasβπ)) & β’ (π β πΏ β (Filβπ)) & β’ (π β πΉ:πβΆπ) & β’ (π β ((π FilMap πΉ)βπ΅) β πΏ) β β’ (π β (π β (fiβπ΅) β ((πΉ β π ) β π‘ β (π‘ β π β π‘ β πΏ)))) | ||
Theorem | fmfnfmlem2 23459* | Lemma for fmfnfm 23462. (Contributed by Jeff Hankins, 19-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ (π β π΅ β (fBasβπ)) & β’ (π β πΏ β (Filβπ)) & β’ (π β πΉ:πβΆπ) & β’ (π β ((π FilMap πΉ)βπ΅) β πΏ) β β’ (π β (βπ₯ β πΏ π = (β‘πΉ β π₯) β ((πΉ β π ) β π‘ β (π‘ β π β π‘ β πΏ)))) | ||
Theorem | fmfnfmlem3 23460* | Lemma for fmfnfm 23462. (Contributed by Jeff Hankins, 19-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ (π β π΅ β (fBasβπ)) & β’ (π β πΏ β (Filβπ)) & β’ (π β πΉ:πβΆπ) & β’ (π β ((π FilMap πΉ)βπ΅) β πΏ) β β’ (π β (fiβran (π₯ β πΏ β¦ (β‘πΉ β π₯))) = ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) | ||
Theorem | fmfnfmlem4 23461* | Lemma for fmfnfm 23462. (Contributed by Jeff Hankins, 19-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ (π β π΅ β (fBasβπ)) & β’ (π β πΏ β (Filβπ)) & β’ (π β πΉ:πβΆπ) & β’ (π β ((π FilMap πΉ)βπ΅) β πΏ) β β’ (π β (π‘ β πΏ β (π‘ β π β§ βπ β (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))(πΉ β π ) β π‘))) | ||
Theorem | fmfnfm 23462* | A filter finer than an image filter is an image filter of the same function. (Contributed by Jeff Hankins, 13-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ (π β π΅ β (fBasβπ)) & β’ (π β πΏ β (Filβπ)) & β’ (π β πΉ:πβΆπ) & β’ (π β ((π FilMap πΉ)βπ΅) β πΏ) β β’ (π β βπ β (Filβπ)(π΅ β π β§ πΏ = ((π FilMap πΉ)βπ))) | ||
Theorem | fmufil 23463 | An image filter of an ultrafilter is an ultrafilter. (Contributed by Jeff Hankins, 11-Dec-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ ((π β π΄ β§ πΏ β (UFilβπ) β§ πΉ:πβΆπ) β ((π FilMap πΉ)βπΏ) β (UFilβπ)) | ||
Theorem | fmid 23464 | The filter map applied to the identity. (Contributed by Jeff Hankins, 8-Nov-2009.) (Revised by Mario Carneiro, 27-Aug-2015.) |
β’ (πΉ β (Filβπ) β ((π FilMap ( I βΎ π))βπΉ) = πΉ) | ||
Theorem | fmco 23465 | Composition of image filters. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ (((π β π β§ π β π β§ π΅ β (fBasβπ)) β§ (πΉ:πβΆπ β§ πΊ:πβΆπ)) β ((π FilMap (πΉ β πΊ))βπ΅) = ((π FilMap πΉ)β((π FilMap πΊ)βπ΅))) | ||
Theorem | ufldom 23466 | The ultrafilter lemma property is a cardinal invariant, so since it transfers to subsets it also transfers over set dominance. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((π β UFL β§ π βΌ π) β π β UFL) | ||
Theorem | flimval 23467* | The set of limit points of a filter. (Contributed by Jeff Hankins, 4-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ πΉ β βͺ ran Fil) β (π½ fLim πΉ) = {π₯ β π β£ (((neiβπ½)β{π₯}) β πΉ β§ πΉ β π« π)}) | ||
Theorem | elflim2 23468 | The predicate "is a limit point of a filter." (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ π = βͺ π½ β β’ (π΄ β (π½ fLim πΉ) β ((π½ β Top β§ πΉ β βͺ ran Fil β§ πΉ β π« π) β§ (π΄ β π β§ ((neiβπ½)β{π΄}) β πΉ))) | ||
Theorem | flimtop 23469 | Reverse closure for the limit point predicate. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
β’ (π΄ β (π½ fLim πΉ) β π½ β Top) | ||
Theorem | flimneiss 23470 | A filter contains the neighborhood filter as a subfilter. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
β’ (π΄ β (π½ fLim πΉ) β ((neiβπ½)β{π΄}) β πΉ) | ||
Theorem | flimnei 23471 | A filter contains all of the neighborhoods of its limit points. (Contributed by Jeff Hankins, 4-Sep-2009.) (Revised by Mario Carneiro, 9-Apr-2015.) |
β’ ((π΄ β (π½ fLim πΉ) β§ π β ((neiβπ½)β{π΄})) β π β πΉ) | ||
Theorem | flimelbas 23472 | A limit point of a filter belongs to its base set. (Contributed by Jeff Hankins, 4-Sep-2009.) (Revised by Mario Carneiro, 9-Apr-2015.) |
β’ π = βͺ π½ β β’ (π΄ β (π½ fLim πΉ) β π΄ β π) | ||
Theorem | flimfil 23473 | Reverse closure for the limit point predicate. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ π = βͺ π½ β β’ (π΄ β (π½ fLim πΉ) β πΉ β (Filβπ)) | ||
Theorem | flimtopon 23474 | Reverse closure for the limit point predicate. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π΄ β (π½ fLim πΉ) β (π½ β (TopOnβπ) β πΉ β (Filβπ))) | ||
Theorem | elflim 23475 | The predicate "is a limit point of a filter." (Contributed by Jeff Hankins, 4-Sep-2009.) (Revised by Mario Carneiro, 23-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β (π΄ β (π½ fLim πΉ) β (π΄ β π β§ ((neiβπ½)β{π΄}) β πΉ))) | ||
Theorem | flimss2 23476 | A limit point of a filter is a limit point of a finer filter. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ πΊ β πΉ) β (π½ fLim πΊ) β (π½ fLim πΉ)) | ||
Theorem | flimss1 23477 | A limit point of a filter is a limit point in a coarser topology. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π½ β πΎ) β (πΎ fLim πΉ) β (π½ fLim πΉ)) | ||
Theorem | neiflim 23478 | A point is a limit point of its neighborhood filter. (Contributed by Jeff Hankins, 7-Sep-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π΄ β (π½ fLim ((neiβπ½)β{π΄}))) | ||
Theorem | flimopn 23479* | The condition for being a limit point of a filter still holds if one only considers open neighborhoods. (Contributed by Jeff Hankins, 4-Sep-2009.) (Proof shortened by Mario Carneiro, 9-Apr-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β (π΄ β (π½ fLim πΉ) β (π΄ β π β§ βπ₯ β π½ (π΄ β π₯ β π₯ β πΉ)))) | ||
Theorem | fbflim 23480* | A condition for a filter to converge to a point involving one of its bases. (Contributed by Jeff Hankins, 4-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ πΉ = (πfilGenπ΅) β β’ ((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β (π΄ β (π½ fLim πΉ) β (π΄ β π β§ βπ₯ β π½ (π΄ β π₯ β βπ¦ β π΅ π¦ β π₯)))) | ||
Theorem | fbflim2 23481* | A condition for a filter base π΅ to converge to a point π΄. Use neighborhoods instead of open neighborhoods. Compare fbflim 23480. (Contributed by FL, 4-Jul-2011.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ πΉ = (πfilGenπ΅) β β’ ((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β (π΄ β (π½ fLim πΉ) β (π΄ β π β§ βπ β ((neiβπ½)β{π΄})βπ₯ β π΅ π₯ β π))) | ||
Theorem | flimclsi 23482 | The convergent points of a filter are a subset of the closure of any of the filter sets. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
β’ (π β πΉ β (π½ fLim πΉ) β ((clsβπ½)βπ)) | ||
Theorem | hausflimlem 23483 | If π΄ and π΅ are both limits of the same filter, then all neighborhoods of π΄ and π΅ intersect. (Contributed by Mario Carneiro, 21-Sep-2015.) |
β’ (((π΄ β (π½ fLim πΉ) β§ π΅ β (π½ fLim πΉ)) β§ (π β π½ β§ π β π½) β§ (π΄ β π β§ π΅ β π)) β (π β© π) β β ) | ||
Theorem | hausflimi 23484* | One direction of hausflim 23485. A filter in a Hausdorff space has at most one limit. (Contributed by FL, 14-Nov-2010.) (Revised by Mario Carneiro, 21-Sep-2015.) |
β’ (π½ β Haus β β*π₯ π₯ β (π½ fLim πΉ)) | ||
Theorem | hausflim 23485* | A condition for a topology to be Hausdorff in terms of filters. A topology is Hausdorff iff every filter has at most one limit point. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ π = βͺ π½ β β’ (π½ β Haus β (π½ β Top β§ βπ β (Filβπ)β*π₯ π₯ β (π½ fLim π))) | ||
Theorem | flimcf 23486* | Fineness is properly characterized by the property that every limit point of a filter in the finer topology is a limit point in the coarser topology. (Contributed by Jeff Hankins, 28-Sep-2009.) (Revised by Mario Carneiro, 23-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π½ β πΎ β βπ β (Filβπ)(πΎ fLim π) β (π½ fLim π))) | ||
Theorem | flimrest 23487 | The set of limit points in a restricted topological space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β ((π½ βΎt π) fLim (πΉ βΎt π)) = ((π½ fLim πΉ) β© π)) | ||
Theorem | flimclslem 23488 | Lemma for flimcls 23489. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ πΉ = (πfilGen(fiβ(((neiβπ½)β{π΄}) βͺ {π}))) β β’ ((π½ β (TopOnβπ) β§ π β π β§ π΄ β ((clsβπ½)βπ)) β (πΉ β (Filβπ) β§ π β πΉ β§ π΄ β (π½ fLim πΉ))) | ||
Theorem | flimcls 23489* | Closure in terms of filter convergence. (Contributed by Jeff Hankins, 28-Nov-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ π β π) β (π΄ β ((clsβπ½)βπ) β βπ β (Filβπ)(π β π β§ π΄ β (π½ fLim π)))) | ||
Theorem | flimsncls 23490 | If π΄ is a limit point of the filter πΉ, then all the points which specialize π΄ (in the specialization preorder) are also limit points. Thus, the set of limit points is a union of closed sets (although this is only nontrivial for non-T1 spaces). (Contributed by Mario Carneiro, 20-Sep-2015.) |
β’ (π΄ β (π½ fLim πΉ) β ((clsβπ½)β{π΄}) β (π½ fLim πΉ)) | ||
Theorem | hauspwpwf1 23491* | Lemma for hauspwpwdom 23492. Points in the closure of a set in a Hausdorff space are characterized by the open neighborhoods they extend into the generating set. (Contributed by Mario Carneiro, 28-Jul-2015.) |
β’ π = βͺ π½ & β’ πΉ = (π₯ β ((clsβπ½)βπ΄) β¦ {π β£ βπ β π½ (π₯ β π β§ π = (π β© π΄))}) β β’ ((π½ β Haus β§ π΄ β π) β πΉ:((clsβπ½)βπ΄)β1-1βπ« π« π΄) | ||
Theorem | hauspwpwdom 23492 | If π is a Hausdorff space, then the cardinality of the closure of a set π΄ is bounded by the double powerset of π΄. In particular, a Hausdorff space with a dense subset π΄ has cardinality at most π« π« π΄, and a separable Hausdorff space has cardinality at most π« π« β. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Mario Carneiro, 28-Jul-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Haus β§ π΄ β π) β ((clsβπ½)βπ΄) βΌ π« π« π΄) | ||
Theorem | flffval 23493* | Given a topology and a filtered set, return the convergence function on the functions from the filtered set to the base set of the topological space. (Contributed by Jeff Hankins, 14-Oct-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ)) β (π½ fLimf πΏ) = (π β (π βm π) β¦ (π½ fLim ((π FilMap π)βπΏ)))) | ||
Theorem | flfval 23494 | Given a function from a filtered set to a topological space, define the set of limit points of the function. (Contributed by Jeff Hankins, 8-Nov-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β ((π½ fLimf πΏ)βπΉ) = (π½ fLim ((π FilMap πΉ)βπΏ))) | ||
Theorem | flfnei 23495* | The property of being a limit point of a function in terms of neighborhoods. (Contributed by Jeff Hankins, 9-Nov-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β (π΄ β ((π½ fLimf πΏ)βπΉ) β (π΄ β π β§ βπ β ((neiβπ½)β{π΄})βπ β πΏ (πΉ β π ) β π))) | ||
Theorem | flfneii 23496* | A neighborhood of a limit point of a function contains the image of a filter element. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ π = βͺ π½ β β’ (((π½ β Top β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β ((π½ fLimf πΏ)βπΉ) β§ π β ((neiβπ½)β{π΄})) β βπ β πΏ (πΉ β π ) β π) | ||
Theorem | isflf 23497* | The property of being a limit point of a function. (Contributed by Jeff Hankins, 8-Nov-2009.) (Revised by Stefan O'Rear, 7-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β (π΄ β ((π½ fLimf πΏ)βπΉ) β (π΄ β π β§ βπ β π½ (π΄ β π β βπ β πΏ (πΉ β π ) β π)))) | ||
Theorem | flfelbas 23498 | A limit point of a function is in the topological space. (Contributed by Jeff Hankins, 10-Nov-2009.) (Revised by Stefan O'Rear, 7-Aug-2015.) |
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β ((π½ fLimf πΏ)βπΉ)) β π΄ β π) | ||
Theorem | flffbas 23499* | Limit points of a function can be defined using filter bases. (Contributed by Jeff Hankins, 9-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.) |
β’ πΏ = (πfilGenπ΅) β β’ ((π½ β (TopOnβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (π΄ β ((π½ fLimf πΏ)βπΉ) β (π΄ β π β§ βπ β π½ (π΄ β π β βπ β π΅ (πΉ β π ) β π)))) | ||
Theorem | flftg 23500* | Limit points of a function can be defined using topological bases. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ π½ = (topGenβπ΅) β β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β (π΄ β ((π½ fLimf πΏ)βπΉ) β (π΄ β π β§ βπ β π΅ (π΄ β π β βπ β πΏ (πΉ β π ) β π)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |