Home | Metamath
Proof Explorer Theorem List (p. 216 of 424) | < 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: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | trfil2 21501* | 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 21502 | Conditions for the trace of a filter 𝐿 to be a filter. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ¬ (𝑌 ∖ 𝐴) ∈ 𝐿)) | ||
Theorem | trfilss 21503 | 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 21504 | 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 21505 | 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 21504 for the converse cancellation law. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ ((𝐹 ∈ (Fil‘𝐴) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉) → ((𝑋filGen𝐹) ↾t 𝐴) = 𝐹) | ||
Theorem | trnei 21506 | 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 21501 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 21507* | 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 21508* | 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 21509* | 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 21510 | 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‘ℤ) | ||
Theorem | uzrest 21511 | 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 21512 | 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 21513 | Extend class notation with the ultrafilters-on-a-set function. |
class UFil | ||
Syntax | cufl 21514 | Extend class notation with the ultrafilter lemma. |
class UFL | ||
Definition | df-ufil 21515* | 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 21516* | Define the class of base sets for which the ultrafilter lemma filssufil 21526 holds. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ UFL = {𝑥 ∣ ∀𝑓 ∈ (Fil‘𝑥)∃𝑔 ∈ (UFil‘𝑥)𝑓 ⊆ 𝑔} | ||
Theorem | isufil 21517* | The property of being an ultrafilter. (Contributed by Jeff Hankins, 30-Nov-2009.) (Revised by Mario Carneiro, 29-Jul-2015.) |
⊢ (𝐹 ∈ (UFil‘𝑋) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ 𝒫 𝑋(𝑥 ∈ 𝐹 ∨ (𝑋 ∖ 𝑥) ∈ 𝐹))) | ||
Theorem | ufilfil 21518 | An ultrafilter is a filter. (Contributed by Jeff Hankins, 1-Dec-2009.) (Revised by Mario Carneiro, 29-Jul-2015.) |
⊢ (𝐹 ∈ (UFil‘𝑋) → 𝐹 ∈ (Fil‘𝑋)) | ||
Theorem | ufilss 21519 | 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 21520 | 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 21521 | 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 21522* | 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 21523 | An ultrafilter is a prime filter. (Contributed by Jeff Hankins, 1-Jan-2010.) (Revised by Mario Carneiro, 2-Aug-2015.) |
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) → ((𝐴 ∈ 𝐹 ∨ 𝐵 ∈ 𝐹) ↔ (𝐴 ∪ 𝐵) ∈ 𝐹)) | ||
Theorem | trufil 21524 | Conditions for the trace of an ultrafilter 𝐿 to be an ultrafilter. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ ((𝐿 ∈ (UFil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝐿 ↾t 𝐴) ∈ (UFil‘𝐴) ↔ 𝐴 ∈ 𝐿)) | ||
Theorem | filssufilg 21525* | A filter is contained in some ultrafilter. This version of filssufil 21526 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 21526* | A filter is contained in some ultrafilter. (Requires the Axiom of Choice, via numth3 9175.) (Contributed by Jeff Hankins, 2-Dec-2009.) (Revised by Stefan O'Rear, 29-Jul-2015.) |
⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓) | ||
Theorem | isufl 21527* | 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 21528* | Property of a set that satisfies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ ((𝑋 ∈ UFL ∧ 𝐹 ∈ (Fil‘𝑋)) → ∃𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓) | ||
Theorem | numufl 21529 | Consequence of filssufilg 21525: a set whose double powerset is well-orderable satisfies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝒫 𝒫 𝑋 ∈ dom card → 𝑋 ∈ UFL) | ||
Theorem | fiufl 21530 | A finite set satisfies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝑋 ∈ Fin → 𝑋 ∈ UFL) | ||
Theorem | acufl 21531 | The axiom of choice implies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (CHOICE → UFL = V) | ||
Theorem | ssufl 21532 | 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 21533* | 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 21534* | 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 21535* | Lemma for fixufil 21536 and uffixfr 21537. (Contributed by Mario Carneiro, 12-Dec-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) → ({{𝐴}} ∈ (fBas‘𝑋) ∧ {𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥} = (𝑋filGen{{𝐴}}))) | ||
Theorem | fixufil 21536* | 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 21537* | 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 21538* | A classification of fixed ultrafilters. (Contributed by Mario Carneiro, 24-May-2015.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
⊢ (𝐹 ∈ (UFil‘𝑋) → (∩ 𝐹 ≠ ∅ ↔ ∃𝑥 ∈ 𝑋 𝐹 = {𝑦 ∈ 𝒫 𝑋 ∣ 𝑥 ∈ 𝑦})) | ||
Theorem | uffixsn 21539 | 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 21540 | 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‘𝑋) → ∩ 𝐹 ≼ 1𝑜) | ||
Theorem | uffinfix 21541* | 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 21542* | An ultrafilter is free iff it contains the Fréchet filter cfinfil 21507 as a subset. (Contributed by NM, 14-Jul-2008.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
⊢ (𝐹 ∈ (UFil‘𝑋) → (∩ 𝐹 = ∅ ↔ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ∈ Fin} ⊆ 𝐹)) | ||
Theorem | ufinffr 21543* | 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 21544* | 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 21545 | 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 21546 | 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 21547 | Extend class definition to include the neighborhood filter mapping function. |
class FilMap | ||
Syntax | cflim 21548 | Extend class notation with a function returning the limit of a filter. |
class fLim | ||
Syntax | cflf 21549 | Extend class definition to include the function for filter-based function limits. |
class fLimf | ||
Syntax | cfcls 21550 | Extend class definition to include the cluster point function on filters. |
class fClus | ||
Syntax | cfcf 21551 | Extend class definition to include the function for cluster points of a function. |
class fClusf | ||
Definition | df-fm 21552* | 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 21553* | 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 21554* | 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 ↦ (𝑓 ∈ (∪ 𝑥 ↑𝑚 ∪ 𝑦) ↦ (𝑥 fLim ((∪ 𝑥 FilMap 𝑓)‘𝑦)))) | ||
Definition | df-fcls 21555* | 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 21556* | Define a function that gives the cluster points of a function. (Contributed by Jeff Hankins, 24-Nov-2009.) |
⊢ fClusf = (𝑗 ∈ Top, 𝑓 ∈ ∪ ran Fil ↦ (𝑔 ∈ (∪ 𝑗 ↑𝑚 ∪ 𝑓) ↦ (𝑗 fClus ((∪ 𝑗 FilMap 𝑔)‘𝑓)))) | ||
Theorem | fmval 21557* | 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 21558 | 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 21559 | Pushing-forward via a function induces a mapping on filters. (Contributed by Stefan O'Rear, 8-Aug-2015.) |
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹:𝑌⟶𝑋) → (𝑋 FilMap 𝐹):(fBas‘𝑌)⟶(Fil‘𝑋)) | ||
Theorem | fmss 21560 | 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 21561* | 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 21562* | 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 21563 | 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 21564* | 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 21565 | 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 21566* | Lemma for rnelfm 21567. (Contributed by Jeff Hankins, 14-Nov-2009.) |
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌)) | ||
Theorem | rnelfm 21567 | 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 21568* | Lemma for fmfnfm 21572. (Contributed by Jeff Hankins, 18-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋)) & ⊢ (𝜑 → 𝐹:𝑌⟶𝑋) & ⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿) ⇒ ⊢ (𝜑 → (𝑠 ∈ (fi‘𝐵) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) | ||
Theorem | fmfnfmlem2 21569* | Lemma for fmfnfm 21572. (Contributed by Jeff Hankins, 19-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋)) & ⊢ (𝜑 → 𝐹:𝑌⟶𝑋) & ⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) | ||
Theorem | fmfnfmlem3 21570* | Lemma for fmfnfm 21572. (Contributed by Jeff Hankins, 19-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋)) & ⊢ (𝜑 → 𝐹:𝑌⟶𝑋) & ⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿) ⇒ ⊢ (𝜑 → (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) = ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) | ||
Theorem | fmfnfmlem4 21571* | Lemma for fmfnfm 21572. (Contributed by Jeff Hankins, 19-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋)) & ⊢ (𝜑 → 𝐹:𝑌⟶𝑋) & ⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿) ⇒ ⊢ (𝜑 → (𝑡 ∈ 𝐿 ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡))) | ||
Theorem | fmfnfm 21572* | 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 21573 | 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 21574 | 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 21575 | Composition of image filters. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) → ((𝑋 FilMap (𝐹 ∘ 𝐺))‘𝐵) = ((𝑋 FilMap 𝐹)‘((𝑌 FilMap 𝐺)‘𝐵))) | ||
Theorem | ufldom 21576 | 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 21577* | 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 21578 | 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 21579 | 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 21580 | 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 21581 | 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 21582 | 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 21583 | 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 21584 | Reverse closure for the limit point predicate. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝐴 ∈ (𝐽 fLim 𝐹) → (𝐽 ∈ (TopOn‘𝑋) ↔ 𝐹 ∈ (Fil‘𝑋))) | ||
Theorem | elflim 21585 | 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 21586 | 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 21587 | 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 21588 | 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 21589* | 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 21590* | 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 21591* | A condition for a filter base 𝐵 to converge to a point 𝐴. Use neighborhoods instead of open neighborhoods. Compare fbflim 21590. (Contributed by FL, 4-Jul-2011.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
⊢ 𝐹 = (𝑋filGen𝐵) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) → (𝐴 ∈ (𝐽 fLim 𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∃𝑥 ∈ 𝐵 𝑥 ⊆ 𝑛))) | ||
Theorem | flimclsi 21592 | 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 21593 | 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 21594* | One direction of hausflim 21595. 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 21595* | 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 21596* | 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 21597 | 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 21598 | Lemma for flimcls 21599. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
⊢ 𝐹 = (𝑋filGen(fi‘(((nei‘𝐽)‘{𝐴}) ∪ {𝑆}))) ⇒ ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ ((cls‘𝐽)‘𝑆)) → (𝐹 ∈ (Fil‘𝑋) ∧ 𝑆 ∈ 𝐹 ∧ 𝐴 ∈ (𝐽 fLim 𝐹))) | ||
Theorem | flimcls 21599* | 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 21600 | 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 𝐹)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |