![]() |
Metamath
Proof Explorer Theorem List (p. 240 of 486) | < 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-30848) |
![]() (30849-32371) |
![]() (32372-48589) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ufprim 23901 | An ultrafilter is a prime filter. (Contributed by Jeff Hankins, 1-Jan-2010.) (Revised by Mario Carneiro, 2-Aug-2015.) |
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) → ((𝐴 ∈ 𝐹 ∨ 𝐵 ∈ 𝐹) ↔ (𝐴 ∪ 𝐵) ∈ 𝐹)) | ||
Theorem | trufil 23902 | Conditions for the trace of an ultrafilter 𝐿 to be an ultrafilter. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ ((𝐿 ∈ (UFil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝐿 ↾t 𝐴) ∈ (UFil‘𝐴) ↔ 𝐴 ∈ 𝐿)) | ||
Theorem | filssufilg 23903* | A filter is contained in some ultrafilter. This version of filssufil 23904 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 23904* | A filter is contained in some ultrafilter. (Requires the Axiom of Choice, via numth3 10504.) (Contributed by Jeff Hankins, 2-Dec-2009.) (Revised by Stefan O'Rear, 29-Jul-2015.) |
⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓) | ||
Theorem | isufl 23905* | 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 23906* | Property of a set that satisfies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ ((𝑋 ∈ UFL ∧ 𝐹 ∈ (Fil‘𝑋)) → ∃𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓) | ||
Theorem | numufl 23907 | Consequence of filssufilg 23903: a set whose double powerset is well-orderable satisfies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝒫 𝒫 𝑋 ∈ dom card → 𝑋 ∈ UFL) | ||
Theorem | fiufl 23908 | A finite set satisfies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝑋 ∈ Fin → 𝑋 ∈ UFL) | ||
Theorem | acufl 23909 | The axiom of choice implies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (CHOICE → UFL = V) | ||
Theorem | ssufl 23910 | 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 23911* | 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 23912* | 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 23913* | Lemma for fixufil 23914 and uffixfr 23915. (Contributed by Mario Carneiro, 12-Dec-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) → ({{𝐴}} ∈ (fBas‘𝑋) ∧ {𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥} = (𝑋filGen{{𝐴}}))) | ||
Theorem | fixufil 23914* | 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 23915* | 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 23916* | A classification of fixed ultrafilters. (Contributed by Mario Carneiro, 24-May-2015.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
⊢ (𝐹 ∈ (UFil‘𝑋) → (∩ 𝐹 ≠ ∅ ↔ ∃𝑥 ∈ 𝑋 𝐹 = {𝑦 ∈ 𝒫 𝑋 ∣ 𝑥 ∈ 𝑦})) | ||
Theorem | uffixsn 23917 | 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 23918 | 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 23919* | 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 23920* | An ultrafilter is free iff it contains the Fréchet filter cfinfil 23885 as a subset. (Contributed by NM, 14-Jul-2008.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
⊢ (𝐹 ∈ (UFil‘𝑋) → (∩ 𝐹 = ∅ ↔ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ∈ Fin} ⊆ 𝐹)) | ||
Theorem | ufinffr 23921* | 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 23922* | 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 23923 | 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 23924 | 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 23925 | Extend class definition to include the neighborhood filter mapping function. |
class FilMap | ||
Syntax | cflim 23926 | Extend class notation with a function returning the limit of a filter. |
class fLim | ||
Syntax | cflf 23927 | Extend class definition to include the function for filter-based function limits. |
class fLimf | ||
Syntax | cfcls 23928 | Extend class definition to include the cluster point function on filters. |
class fClus | ||
Syntax | cfcf 23929 | Extend class definition to include the function for cluster points of a function. |
class fClusf | ||
Definition | df-fm 23930* | 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 23931* | 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 23932* | 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 23933* | 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 23934* | 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 23935* | 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 23936 | 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 23937 | Pushing-forward via a function induces a mapping on filters. (Contributed by Stefan O'Rear, 8-Aug-2015.) |
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹:𝑌⟶𝑋) → (𝑋 FilMap 𝐹):(fBas‘𝑌)⟶(Fil‘𝑋)) | ||
Theorem | fmss 23938 | 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 23939* | 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 23940* | 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 23941 | 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 23942* | 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 23943 | 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 23944* | Lemma for rnelfm 23945. (Contributed by Jeff Hankins, 14-Nov-2009.) |
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌)) | ||
Theorem | rnelfm 23945 | 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 23946* | Lemma for fmfnfm 23950. (Contributed by Jeff Hankins, 18-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋)) & ⊢ (𝜑 → 𝐹:𝑌⟶𝑋) & ⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿) ⇒ ⊢ (𝜑 → (𝑠 ∈ (fi‘𝐵) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) | ||
Theorem | fmfnfmlem2 23947* | Lemma for fmfnfm 23950. (Contributed by Jeff Hankins, 19-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋)) & ⊢ (𝜑 → 𝐹:𝑌⟶𝑋) & ⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) | ||
Theorem | fmfnfmlem3 23948* | Lemma for fmfnfm 23950. (Contributed by Jeff Hankins, 19-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋)) & ⊢ (𝜑 → 𝐹:𝑌⟶𝑋) & ⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿) ⇒ ⊢ (𝜑 → (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) = ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) | ||
Theorem | fmfnfmlem4 23949* | Lemma for fmfnfm 23950. (Contributed by Jeff Hankins, 19-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋)) & ⊢ (𝜑 → 𝐹:𝑌⟶𝑋) & ⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿) ⇒ ⊢ (𝜑 → (𝑡 ∈ 𝐿 ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡))) | ||
Theorem | fmfnfm 23950* | 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 23951 | 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 23952 | 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 23953 | Composition of image filters. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) → ((𝑋 FilMap (𝐹 ∘ 𝐺))‘𝐵) = ((𝑋 FilMap 𝐹)‘((𝑌 FilMap 𝐺)‘𝐵))) | ||
Theorem | ufldom 23954 | 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 23955* | 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 23956 | 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 23957 | 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 23958 | 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 23959 | 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 23960 | 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 23961 | 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 23962 | Reverse closure for the limit point predicate. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝐴 ∈ (𝐽 fLim 𝐹) → (𝐽 ∈ (TopOn‘𝑋) ↔ 𝐹 ∈ (Fil‘𝑋))) | ||
Theorem | elflim 23963 | 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 23964 | 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 23965 | 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 23966 | 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 23967* | 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 23968* | 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 23969* | A condition for a filter base 𝐵 to converge to a point 𝐴. Use neighborhoods instead of open neighborhoods. Compare fbflim 23968. (Contributed by FL, 4-Jul-2011.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
⊢ 𝐹 = (𝑋filGen𝐵) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛))) | ||
Theorem | flimclsi 23970 | 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 23971 | 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 23972* | One direction of hausflim 23973. 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 23973* | 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 23974* | 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 23975 | 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 23976 | Lemma for flimcls 23977. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
⊢ 𝐹 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝐹 ∈ (Fil‘𝑋) ∧ 𝑆 ∈ 𝐹 ∧ 𝐴 ∈ (𝐽 fLim 𝐹))) | ||
Theorem | flimcls 23977* | 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 23978 | 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 23979* | Lemma for hauspwpwdom 23980. 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 23980 | 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 23981* | 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 23982 | 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 23983* | 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 23984* | 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 23985* | 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 23986 | 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 23987* | 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 23988* | Limit points of a function can be defined using topological bases. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ 𝐽 = (topGen‘𝐵) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐵 (𝐴 ∈ 𝑜 → ∃𝑠 ∈ 𝐿 (𝐹 “ 𝑠) ⊆ 𝑜)))) | ||
Theorem | hausflf 23989* | If a function has its values in a Hausdorff space, then it has at most one limit value. (Contributed by FL, 14-Nov-2010.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Haus ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ∃*𝑥 𝑥 ∈ ((𝐽 fLimf 𝐿)‘𝐹)) | ||
Theorem | hausflf2 23990 | If a convergent function has its values in a Hausdorff space, then it has a unique limit. (Contributed by FL, 14-Nov-2010.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (((𝐽 ∈ Haus ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ ((𝐽 fLimf 𝐿)‘𝐹) ≠ ∅) → ((𝐽 fLimf 𝐿)‘𝐹) ≈ 1o) | ||
Theorem | cnpflfi 23991 | Forward direction of cnpflf 23993. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
⊢ ((𝐴 ∈ (𝐽 fLim 𝐿) ∧ 𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴)) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝐿)‘𝐹)) | ||
Theorem | cnpflf2 23992 | 𝐹 is continuous at point 𝐴 iff a limit of 𝐹 when 𝑥 tends to 𝐴 is (𝐹‘𝐴). Proposition 9 of [BourbakiTop1] p. TG I.50. (Contributed by FL, 29-May-2011.) (Revised by Mario Carneiro, 9-Apr-2015.) |
⊢ 𝐿 = ((nei‘𝐽)‘{𝐴}) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝐿)‘𝐹)))) | ||
Theorem | cnpflf 23993* | Continuity of a function at a point in terms of filter limits. (Contributed by Jeff Hankins, 7-Sep-2009.) (Revised by Stefan O'Rear, 7-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝐴) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐴 ∈ (𝐽 fLim 𝑓) → (𝐹‘𝐴) ∈ ((𝐾 fLimf 𝑓)‘𝐹))))) | ||
Theorem | cnflf 23994* | A function is continuous iff it respects filter limits. (Contributed by Jeff Hankins, 6-Sep-2009.) (Revised by Stefan O'Rear, 7-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)∀𝑥 ∈ (𝐽 fLim 𝑓)(𝐹‘𝑥) ∈ ((𝐾 fLimf 𝑓)‘𝐹)))) | ||
Theorem | cnflf2 23995* | A function is continuous iff it respects filter limits. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓 ∈ (Fil‘𝑋)(𝐹 “ (𝐽 fLim 𝑓)) ⊆ ((𝐾 fLimf 𝑓)‘𝐹)))) | ||
Theorem | flfcnp 23996 | A continuous function preserves filter limits. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐴))) → (𝐺‘𝐴) ∈ ((𝐾 fLimf 𝐿)‘(𝐺 ∘ 𝐹))) | ||
Theorem | lmflf 23997 | The topological limit relation on functions can be written in terms of the filter limit along the filter generated by the upper integer sets. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐿 = (𝑍filGen(ℤ≥ “ 𝑍)) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶𝑋) → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝑃 ∈ ((𝐽 fLimf 𝐿)‘𝐹))) | ||
Theorem | txflf 23998* | Two sequences converge in a filter iff the sequence of their ordered pairs converges. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑍)) & ⊢ (𝜑 → 𝐹:𝑍⟶𝑋) & ⊢ (𝜑 → 𝐺:𝑍⟶𝑌) & ⊢ 𝐻 = (𝑛 ∈ 𝑍 ↦ 〈(𝐹‘𝑛), (𝐺‘𝑛)〉) ⇒ ⊢ (𝜑 → (〈𝑅, 𝑆〉 ∈ (((𝐽 ×t 𝐾) fLimf 𝐿)‘𝐻) ↔ (𝑅 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ∧ 𝑆 ∈ ((𝐾 fLimf 𝐿)‘𝐺)))) | ||
Theorem | flfcnp2 23999* | The image of a convergent sequence under a continuous map is convergent to the image of the original point. Binary operation version. (Contributed by Mario Carneiro, 19-Sep-2015.) |
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑍)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐴 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑍) → 𝐵 ∈ 𝑌) & ⊢ (𝜑 → 𝑅 ∈ ((𝐽 fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ 𝐴))) & ⊢ (𝜑 → 𝑆 ∈ ((𝐾 fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ 𝐵))) & ⊢ (𝜑 → 𝑂 ∈ (((𝐽 ×t 𝐾) CnP 𝑁)‘〈𝑅, 𝑆〉)) ⇒ ⊢ (𝜑 → (𝑅𝑂𝑆) ∈ ((𝑁 fLimf 𝐿)‘(𝑥 ∈ 𝑍 ↦ (𝐴𝑂𝐵)))) | ||
Theorem | fclsval 24000* | The set of all cluster points of a filter. (Contributed by Jeff Hankins, 10-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐹 ∈ (Fil‘𝑌)) → (𝐽 fClus 𝐹) = if(𝑋 = 𝑌, ∩ 𝑡 ∈ 𝐹 ((cls‘𝐽)‘𝑡), ∅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |