Home | Metamath
Proof Explorer Theorem List (p. 225 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | infil 22401 | The intersection of two filters is a filter. Use fiint 8784 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 22402 | 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 22403 | 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 22404 | Condition for a singleton to be a filter base. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐵 ∈ 𝑉) → {𝐴} ∈ (fBas‘𝐵)) | ||
Theorem | fsubbas 22405 | 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 22406 | 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 22407* | 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 22408* | 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 22409* | 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 22410 | 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 22411 | 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 22412* | 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 22413 | A filter generates itself. (Contributed by Jeff Hankins, 5-Sep-2009.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑋filGen𝐹) = 𝐹) | ||
Theorem | elfilss 22414* | An element belongs to a filter iff any element below it does. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐴 ∈ 𝐹 ↔ ∃𝑡 ∈ 𝐹 𝑡 ⊆ 𝐴)) | ||
Theorem | filfinnfr 22415 | 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 22416 | 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 22417 | Absorption law for filter generation. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹)) | ||
Theorem | neifil 22418 | 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 22419 | Recover the base set from a filter. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
⊢ (𝐹 ∈ (Fil‘𝑋) → ∪ 𝐹 = 𝑋) | ||
Theorem | filunirn 22420 | Two ways to express a filter on an unspecified base. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
⊢ (𝐹 ∈ ∪ ran Fil ↔ 𝐹 ∈ (Fil‘∪ 𝐹)) | ||
Theorem | filconn 22421 | 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 22422* | 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 22423* | 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 22424 | 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 22425* | 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 22426 | Conditions for the trace of a filter 𝐿 to be a filter. (Contributed by Stefan O'Rear, 2-Aug-2015.) |
⊢ ((𝐿 ∈ (Fil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝐿 ↾t 𝐴) ∈ (Fil‘𝐴) ↔ ¬ (𝑌 ∖ 𝐴) ∈ 𝐿)) | ||
Theorem | trfilss 22427 | 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 22428 | 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 22429 | 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 22428 for the converse cancellation law. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ ((𝐹 ∈ (Fil‘𝐴) ∧ 𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝑉) → ((𝑋filGen𝐹) ↾t 𝐴) = 𝐹) | ||
Theorem | trnei 22430 | 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 22425 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 22431* | 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 22432* | 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 22433* | 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 22434 | 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 22435 | 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 22436 | 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 22437 | Extend class notation with the ultrafilters-on-a-set function. |
class UFil | ||
Syntax | cufl 22438 | Extend class notation with the ultrafilter lemma. |
class UFL | ||
Definition | df-ufil 22439* | 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 22440* | Define the class of base sets for which the ultrafilter lemma filssufil 22450 holds. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ UFL = {𝑥 ∣ ∀𝑓 ∈ (Fil‘𝑥)∃𝑔 ∈ (UFil‘𝑥)𝑓 ⊆ 𝑔} | ||
Theorem | isufil 22441* | The property of being an ultrafilter. (Contributed by Jeff Hankins, 30-Nov-2009.) (Revised by Mario Carneiro, 29-Jul-2015.) |
⊢ (𝐹 ∈ (UFil‘𝑋) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ 𝒫 𝑋(𝑥 ∈ 𝐹 ∨ (𝑋 ∖ 𝑥) ∈ 𝐹))) | ||
Theorem | ufilfil 22442 | An ultrafilter is a filter. (Contributed by Jeff Hankins, 1-Dec-2009.) (Revised by Mario Carneiro, 29-Jul-2015.) |
⊢ (𝐹 ∈ (UFil‘𝑋) → 𝐹 ∈ (Fil‘𝑋)) | ||
Theorem | ufilss 22443 | 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 22444 | 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 22445 | 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 22446* | 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 22447 | An ultrafilter is a prime filter. (Contributed by Jeff Hankins, 1-Jan-2010.) (Revised by Mario Carneiro, 2-Aug-2015.) |
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑋) → ((𝐴 ∈ 𝐹 ∨ 𝐵 ∈ 𝐹) ↔ (𝐴 ∪ 𝐵) ∈ 𝐹)) | ||
Theorem | trufil 22448 | Conditions for the trace of an ultrafilter 𝐿 to be an ultrafilter. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ ((𝐿 ∈ (UFil‘𝑌) ∧ 𝐴 ⊆ 𝑌) → ((𝐿 ↾t 𝐴) ∈ (UFil‘𝐴) ↔ 𝐴 ∈ 𝐿)) | ||
Theorem | filssufilg 22449* | A filter is contained in some ultrafilter. This version of filssufil 22450 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 22450* | A filter is contained in some ultrafilter. (Requires the Axiom of Choice, via numth3 9881.) (Contributed by Jeff Hankins, 2-Dec-2009.) (Revised by Stefan O'Rear, 29-Jul-2015.) |
⊢ (𝐹 ∈ (Fil‘𝑋) → ∃𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓) | ||
Theorem | isufl 22451* | 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 22452* | Property of a set that satisfies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ ((𝑋 ∈ UFL ∧ 𝐹 ∈ (Fil‘𝑋)) → ∃𝑓 ∈ (UFil‘𝑋)𝐹 ⊆ 𝑓) | ||
Theorem | numufl 22453 | Consequence of filssufilg 22449: a set whose double powerset is well-orderable satisfies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝒫 𝒫 𝑋 ∈ dom card → 𝑋 ∈ UFL) | ||
Theorem | fiufl 22454 | A finite set satisfies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (𝑋 ∈ Fin → 𝑋 ∈ UFL) | ||
Theorem | acufl 22455 | The axiom of choice implies the ultrafilter lemma. (Contributed by Mario Carneiro, 26-Aug-2015.) |
⊢ (CHOICE → UFL = V) | ||
Theorem | ssufl 22456 | 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 22457* | 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 22458* | 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 22459* | Lemma for fixufil 22460 and uffixfr 22461. (Contributed by Mario Carneiro, 12-Dec-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋) → ({{𝐴}} ∈ (fBas‘𝑋) ∧ {𝑥 ∈ 𝒫 𝑋 ∣ 𝐴 ∈ 𝑥} = (𝑋filGen{{𝐴}}))) | ||
Theorem | fixufil 22460* | 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 22461* | 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 22462* | A classification of fixed ultrafilters. (Contributed by Mario Carneiro, 24-May-2015.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
⊢ (𝐹 ∈ (UFil‘𝑋) → (∩ 𝐹 ≠ ∅ ↔ ∃𝑥 ∈ 𝑋 𝐹 = {𝑦 ∈ 𝒫 𝑋 ∣ 𝑥 ∈ 𝑦})) | ||
Theorem | uffixsn 22463 | 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 22464 | 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 22465* | 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 22466* | An ultrafilter is free iff it contains the Fréchet filter cfinfil 22431 as a subset. (Contributed by NM, 14-Jul-2008.) (Revised by Stefan O'Rear, 2-Aug-2015.) |
⊢ (𝐹 ∈ (UFil‘𝑋) → (∩ 𝐹 = ∅ ↔ {𝑥 ∈ 𝒫 𝑋 ∣ (𝑋 ∖ 𝑥) ∈ Fin} ⊆ 𝐹)) | ||
Theorem | ufinffr 22467* | 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 22468* | 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 22469 | 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 22470 | 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 22471 | Extend class definition to include the neighborhood filter mapping function. |
class FilMap | ||
Syntax | cflim 22472 | Extend class notation with a function returning the limit of a filter. |
class fLim | ||
Syntax | cflf 22473 | Extend class definition to include the function for filter-based function limits. |
class fLimf | ||
Syntax | cfcls 22474 | Extend class definition to include the cluster point function on filters. |
class fClus | ||
Syntax | cfcf 22475 | Extend class definition to include the function for cluster points of a function. |
class fClusf | ||
Definition | df-fm 22476* | 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 22477* | 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 22478* | 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 22479* | 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 22480* | 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 22481* | 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 22482 | 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 22483 | Pushing-forward via a function induces a mapping on filters. (Contributed by Stefan O'Rear, 8-Aug-2015.) |
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝐹:𝑌⟶𝑋) → (𝑋 FilMap 𝐹):(fBas‘𝑌)⟶(Fil‘𝑋)) | ||
Theorem | fmss 22484 | 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 22485* | 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 22486* | 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 22487 | 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 22488* | 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 22489 | 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 22490* | Lemma for rnelfm 22491. (Contributed by Jeff Hankins, 14-Nov-2009.) |
⊢ (((𝑌 ∈ 𝐴 ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌)) | ||
Theorem | rnelfm 22491 | 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 22492* | Lemma for fmfnfm 22496. (Contributed by Jeff Hankins, 18-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋)) & ⊢ (𝜑 → 𝐹:𝑌⟶𝑋) & ⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿) ⇒ ⊢ (𝜑 → (𝑠 ∈ (fi‘𝐵) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) | ||
Theorem | fmfnfmlem2 22493* | Lemma for fmfnfm 22496. (Contributed by Jeff Hankins, 19-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋)) & ⊢ (𝜑 → 𝐹:𝑌⟶𝑋) & ⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿) ⇒ ⊢ (𝜑 → (∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) | ||
Theorem | fmfnfmlem3 22494* | Lemma for fmfnfm 22496. (Contributed by Jeff Hankins, 19-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋)) & ⊢ (𝜑 → 𝐹:𝑌⟶𝑋) & ⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿) ⇒ ⊢ (𝜑 → (fi‘ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) = ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) | ||
Theorem | fmfnfmlem4 22495* | Lemma for fmfnfm 22496. (Contributed by Jeff Hankins, 19-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋)) & ⊢ (𝜑 → 𝐹:𝑌⟶𝑋) & ⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿) ⇒ ⊢ (𝜑 → (𝑡 ∈ 𝐿 ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡))) | ||
Theorem | fmfnfm 22496* | 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 22497 | 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 22498 | 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 22499 | Composition of image filters. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝐵 ∈ (fBas‘𝑍)) ∧ (𝐹:𝑌⟶𝑋 ∧ 𝐺:𝑍⟶𝑌)) → ((𝑋 FilMap (𝐹 ∘ 𝐺))‘𝐵) = ((𝑋 FilMap 𝐹)‘((𝑌 FilMap 𝐺)‘𝐵))) | ||
Theorem | ufldom 22500 | 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) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |