mathlib3 documentation

order.filter.bases

Filter bases #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A filter basis B : filter_basis α on a type α is a nonempty collection of sets of α such that the intersection of two elements of this collection contains some element of the collection. Compared to filters, filter bases do not require that any set containing an element of B belongs to B. A filter basis B can be used to construct B.filter : filter α such that a set belongs to B.filter if and only if it contains an element of B.

Given an indexing type ι, a predicate p : ι → Prop, and a map s : ι → set α, the proposition h : filter.is_basis p s makes sure the range of s bounded by p (ie. s '' set_of p) defines a filter basis h.filter_basis.

If one already has a filter l on α, filter.has_basis l p s (where p : ι → Prop and s : ι → set α as above) means that a set belongs to l if and only if it contains some s i with p i. It implies h : filter.is_basis p s, and l = h.filter_basis.filter. The point of this definition is that checking statements involving elements of l often reduces to checking them on the basis elements.

We define a function has_basis.index (h : filter.has_basis l p s) (t) (ht : t ∈ l) that returns some index i such that p i and s i ⊆ t. This function can be useful to avoid manual destruction of h.mem_iff.mpr ht using cases or let.

This file also introduces more restricted classes of bases, involving monotonicity or countability. In particular, for l : filter α, l.is_countably_generated means there is a countable set of sets which generates s. This is reformulated in term of bases, and consequences are derived.

Main statements #

Implementation notes #

As with Union/bUnion/sUnion, there are three different approaches to filter bases:

We use the latter one because, e.g., 𝓝 x in an emetric_space or in a metric_space has a basis of this form. The other two can be emulated using s = id or p = λ _, true.

With this approach sometimes one needs to simp the statement provided by the has_basis machinery, e.g., simp only [exists_prop, true_and] or simp only [forall_const] can help with the case p = λ _, true.

source
structure filter_basis (α : Type u_6) :
Type u_6

A filter basis B on a type α is a nonempty collection of sets of α such that the intersection of two elements of this collection contains some element of the collection.

Instances for filter_basis
source
@[protected, instance]
def filter_basis.nonempty_sets {α : Type u_1} (B : filter_basis α) :
nonempty ↥(B.sets)
source
@[protected, instance, reducible]
def filter_basis.has_mem {α : Type u_1} :
has_mem (set α) (filter_basis α)

If B is a filter basis on α, and U a subset of α then we can write U ∈ B as on paper.

Equations
source
@[protected, instance]
def filter_basis.inhabited  :
inhabited (filter_basis ℕ)
Equations
source
def filter.as_basis {α : Type u_1} (f : filter α) :
filter_basis α

View a filter as a filter basis.

Equations
source
structure filter.is_basis {α : Type u_1} {ι : Sort u_4} (p : ι → Prop) (s : ι → set α) :
Prop

is_basis p s means the image of s bounded by p is a filter basis.

source
@[protected]
def filter.is_basis.filter_basis {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → set α} (h : filter.is_basis p s) :
filter_basis α

Constructs a filter basis from an indexed family of sets satisfying is_basis.

Equations
source
theorem filter.is_basis.mem_filter_basis_iff {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → set α} (h : filter.is_basis p s) {U : set α} :
U ∈ h.filter_basis ↔ ∃ (i : ι), p i ∧ s i = U
source
@[protected]
def filter_basis.filter {α : Type u_1} (B : filter_basis α) :
filter α

The filter associated to a filter basis.

Equations
source
theorem filter_basis.mem_filter_iff {α : Type u_1} (B : filter_basis α) {U : set α} :
U ∈ B.filter ↔ ∃ (s : set α) (H : s ∈ B), s ⊆ U
source
theorem filter_basis.mem_filter_of_mem {α : Type u_1} (B : filter_basis α) {U : set α} :
U ∈ B → U ∈ B.filter
source
theorem filter_basis.eq_infi_principal {α : Type u_1} (B : filter_basis α) :
B.filter = ⨅ (s : ↥(B.sets)), filter.principal ↑s
source
@[protected]
theorem filter_basis.generate {α : Type u_1} (B : filter_basis α) :
filter.generate B.sets = B.filter
source
@[protected]
def filter.is_basis.filter {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → set α} (h : filter.is_basis p s) :
filter α

Constructs a filter from an indexed family of sets satisfying is_basis.

Equations
source
@[protected]
theorem filter.is_basis.mem_filter_iff {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → set α} (h : filter.is_basis p s) {U : set α} :
U ∈ h.filter ↔ ∃ (i : ι), p i ∧ s i ⊆ U
source
theorem filter.is_basis.filter_eq_generate {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → set α} (h : filter.is_basis p s) :
h.filter = filter.generate {U : set α | ∃ (i : ι), p i ∧ s i = U}
source
structure filter.has_basis {α : Type u_1} {ι : Sort u_4} (l : filter α) (p : ι → Prop) (s : ι → set α) :
Prop

We say that a filter l has a basis s : ι → set α bounded by p : ι → Prop, if t ∈ l if and only if t includes s i for some i such that p i.

source
theorem filter.has_basis_generate {α : Type u_1} (s : set (set α)) :
(filter.generate s).has_basis (λ (t : set (set α)), t.finite ∧ t ⊆ s) (λ (t : set (set α)), ⋂₀ t)
source
def filter.filter_basis.of_sets {α : Type u_1} (s : set (set α)) :
filter_basis α

The smallest filter basis containing a given collection of sets.

Equations
source
theorem filter.has_basis.mem_iff {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} {t : set α} (hl : l.has_basis p s) :
t ∈ l ↔ ∃ (i : ι) (hi : p i), s i ⊆ t

Definition of has_basis unfolded with implicit set argument.

source
theorem filter.has_basis.eq_of_same_basis {α : Type u_1} {ι : Sort u_4} {l l' : filter α} {p : ι → Prop} {s : ι → set α} (hl : l.has_basis p s) (hl' : l'.has_basis p s) :
l = l'
source
theorem filter.has_basis_iff {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} :
l.has_basis p s ↔ ∀ (t : set α), t ∈ l ↔ ∃ (i : ι) (hi : p i), s i ⊆ t
source
theorem filter.has_basis.ex_mem {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} (h : l.has_basis p s) :
∃ (i : ι), p i
source
@[protected]
theorem filter.has_basis.nonempty {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} (h : l.has_basis p s) :
nonempty ι
source
@[protected]
theorem filter.is_basis.has_basis {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → set α} (h : filter.is_basis p s) :
h.filter.has_basis p s
source
theorem filter.has_basis.mem_of_superset {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} {t : set α} {i : ι} (hl : l.has_basis p s) (hi : p i) (ht : s i ⊆ t) :
t ∈ l
source
theorem filter.has_basis.mem_of_mem {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} {i : ι} (hl : l.has_basis p s) (hi : p i) :
s i ∈ l
source
noncomputable def filter.has_basis.index {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} (h : l.has_basis p s) (t : set α) (ht : t ∈ l) :
{i // p i}

Index of a basis set such that s i ⊆ t as an element of subtype p.

Equations
source
theorem filter.has_basis.property_index {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} {t : set α} (h : l.has_basis p s) (ht : t ∈ l) :
p ↑(h.index t ht)
source
theorem filter.has_basis.set_index_mem {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} {t : set α} (h : l.has_basis p s) (ht : t ∈ l) :
s ↑(h.index t ht) ∈ l
source
theorem filter.has_basis.set_index_subset {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} {t : set α} (h : l.has_basis p s) (ht : t ∈ l) :
s ↑(h.index t ht) ⊆ t
source
theorem filter.has_basis.is_basis {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} (h : l.has_basis p s) :
filter.is_basis p s
source
theorem filter.has_basis.filter_eq {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} (h : l.has_basis p s) :
_.filter = l
source
theorem filter.has_basis.eq_generate {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} (h : l.has_basis p s) :
l = filter.generate {U : set α | ∃ (i : ι), p i ∧ s i = U}
source
theorem filter.generate_eq_generate_inter {α : Type u_1} (s : set (set α)) :
filter.generate s = filter.generate (set.sInter '' {t : set (set α) | t.finite ∧ t ⊆ s})
source
theorem filter.of_sets_filter_eq_generate {α : Type u_1} (s : set (set α)) :
(filter.filter_basis.of_sets s).filter = filter.generate s
source
@[protected]
theorem filter_basis.has_basis {α : Type u_1} (B : filter_basis α) :
B.filter.has_basis (λ (s : set α), s ∈ B) id
source
theorem filter.has_basis.to_has_basis' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l : filter α} {p : ι → Prop} {s : ι → set α} {p' : ι' → Prop} {s' : ι' → set α} (hl : l.has_basis p s) (h : ∀ (i : ι), p i → (∃ (i' : ι'), p' i' ∧ s' i' ⊆ s i)) (h' : ∀ (i' : ι'), p' i' → s' i' ∈ l) :
l.has_basis p' s'
source
theorem filter.has_basis.to_has_basis {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l : filter α} {p : ι → Prop} {s : ι → set α} {p' : ι' → Prop} {s' : ι' → set α} (hl : l.has_basis p s) (h : ∀ (i : ι), p i → (∃ (i' : ι'), p' i' ∧ s' i' ⊆ s i)) (h' : ∀ (i' : ι'), p' i' → (∃ (i : ι), p i ∧ s i ⊆ s' i')) :
l.has_basis p' s'
source
theorem filter.has_basis.to_subset {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} (hl : l.has_basis p s) {t : ι → set α} (h : ∀ (i : ι), p i → t i ⊆ s i) (ht : ∀ (i : ι), p i → t i ∈ l) :
l.has_basis p t
source
theorem filter.has_basis.eventually_iff {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} (hl : l.has_basis p s) {q : α → Prop} :
(∀ᶠ (x : α) in l, q x) ↔ ∃ (i : ι), p i ∧ ∀ ⦃x : α⦄, x ∈ s i → q x
source
theorem filter.has_basis.frequently_iff {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} (hl : l.has_basis p s) {q : α → Prop} :
(∃ᶠ (x : α) in l, q x) ↔ ∀ (i : ι), p i → (∃ (x : α) (H : x ∈ s i), q x)
source
theorem filter.has_basis.exists_iff {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} (hl : l.has_basis p s) {P : set α → Prop} (mono : ∀ ⦃s t : set α⦄, s ⊆ t → P t → P s) :
(∃ (s : set α) (H : s ∈ l), P s) ↔ ∃ (i : ι) (hi : p i), P (s i)
source
theorem filter.has_basis.forall_iff {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} (hl : l.has_basis p s) {P : set α → Prop} (mono : ∀ ⦃s t : set α⦄, s ⊆ t → P s → P t) :
(∀ (s : set α), s ∈ l → P s) ↔ ∀ (i : ι), p i → P (s i)
source
theorem filter.has_basis.ne_bot_iff {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} (hl : l.has_basis p s) :
l.ne_bot ↔ ∀ {i : ι}, p i → (s i).nonempty
source
theorem filter.has_basis.eq_bot_iff {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} (hl : l.has_basis p s) :
l = ⊥ ↔ ∃ (i : ι), p i ∧ s i = ∅
source
theorem filter.generate_ne_bot_iff {α : Type u_1} {s : set (set α)} :
(filter.generate s).ne_bot ↔ ∀ (t : set (set α)), t ⊆ s → t.finite → (⋂₀ t).nonempty
source
theorem filter.basis_sets {α : Type u_1} (l : filter α) :
l.has_basis (λ (s : set α), s ∈ l) id
source
theorem filter.as_basis_filter {α : Type u_1} (f : filter α) :
f.as_basis.filter = f
source
theorem filter.has_basis_self {α : Type u_1} {l : filter α} {P : set α → Prop} :
l.has_basis (λ (s : set α), s ∈ l ∧ P s) id ↔ ∀ (t : set α), t ∈ l → (∃ (r : set α) (H : r ∈ l), P r ∧ r ⊆ t)
source
theorem filter.has_basis.comp_surjective {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l : filter α} {p : ι → Prop} {s : ι → set α} (h : l.has_basis p s) {g : ι' → ι} (hg : function.surjective g) :
l.has_basis (p ∘ g) (s ∘ g)
source
theorem filter.has_basis.comp_equiv {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l : filter α} {p : ι → Prop} {s : ι → set α} (h : l.has_basis p s) (e : ι' ≃ ι) :
l.has_basis (p ∘ ⇑e) (s ∘ ⇑e)
source
theorem filter.has_basis.restrict {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} (h : l.has_basis p s) {q : ι → Prop} (hq : ∀ (i : ι), p i → (∃ (j : ι), p j ∧ q j ∧ s j ⊆ s i)) :
l.has_basis (λ (i : ι), p i ∧ q i) s

If {s i | p i} is a basis of a filter l and each s i includes s j such that p j ∧ q j, then {s j | p j ∧ q j} is a basis of l.

source
theorem filter.has_basis.restrict_subset {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} (h : l.has_basis p s) {V : set α} (hV : V ∈ l) :
l.has_basis (λ (i : ι), p i ∧ s i ⊆ V) s

If {s i | p i} is a basis of a filter l and V ∈ l, then {s i | p i ∧ s i ⊆ V} is a basis of l.

source
theorem filter.has_basis.has_basis_self_subset {α : Type u_1} {l : filter α} {p : set α → Prop} (h : l.has_basis (λ (s : set α), s ∈ l ∧ p s) id) {V : set α} (hV : V ∈ l) :
l.has_basis (λ (s : set α), s ∈ l ∧ p s ∧ s ⊆ V) id
source
theorem filter.has_basis.ge_iff {α : Type u_1} {ι' : Sort u_5} {l l' : filter α} {p' : ι' → Prop} {s' : ι' → set α} (hl' : l'.has_basis p' s') :
l ≤ l' ↔ ∀ (i' : ι'), p' i' → s' i' ∈ l
source
theorem filter.has_basis.le_iff {α : Type u_1} {ι : Sort u_4} {l l' : filter α} {p : ι → Prop} {s : ι → set α} (hl : l.has_basis p s) :
l ≤ l' ↔ ∀ (t : set α), t ∈ l' → (∃ (i : ι) (hi : p i), s i ⊆ t)
source
theorem filter.has_basis.le_basis_iff {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l l' : filter α} {p : ι → Prop} {s : ι → set α} {p' : ι' → Prop} {s' : ι' → set α} (hl : l.has_basis p s) (hl' : l'.has_basis p' s') :
l ≤ l' ↔ ∀ (i' : ι'), p' i' → (∃ (i : ι) (hi : p i), s i ⊆ s' i')
source
theorem filter.has_basis.ext {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l l' : filter α} {p : ι → Prop} {s : ι → set α} {p' : ι' → Prop} {s' : ι' → set α} (hl : l.has_basis p s) (hl' : l'.has_basis p' s') (h : ∀ (i : ι), p i → (∃ (i' : ι'), p' i' ∧ s' i' ⊆ s i)) (h' : ∀ (i' : ι'), p' i' → (∃ (i : ι), p i ∧ s i ⊆ s' i')) :
l = l'
source
theorem filter.has_basis.inf' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l l' : filter α} {p : ι → Prop} {s : ι → set α} {p' : ι' → Prop} {s' : ι' → set α} (hl : l.has_basis p s) (hl' : l'.has_basis p' s') :
(l ⊓ l').has_basis (λ (i : pprod ι ι'), p i.fst ∧ p' i.snd) (λ (i : pprod ι ι'), s i.fst ∩ s' i.snd)
source
theorem filter.has_basis.inf {α : Type u_1} {l l' : filter α} {ι : Type u_2} {ι' : Type u_3} {p : ι → Prop} {s : ι → set α} {p' : ι' → Prop} {s' : ι' → set α} (hl : l.has_basis p s) (hl' : l'.has_basis p' s') :
(l ⊓ l').has_basis (λ (i : ι × ι'), p i.fst ∧ p' i.snd) (λ (i : ι × ι'), s i.fst ∩ s' i.snd)
source
theorem filter.has_basis_infi' {α : Type u_1} {ι : Type u_2} {ι' : ι → Type u_3} {l : ι → filter α} {p : Π (i : ι), ι' i → Prop} {s : Π (i : ι), ι' i → set α} (hl : ∀ (i : ι), (l i).has_basis (p i) (s i)) :
(⨅ (i : ι), l i).has_basis (λ (If : set ι × Π (i : ι), ι' i), If.fst.finite ∧ ∀ (i : ι), i ∈ If.fst → p i (If.snd i)) (λ (If : set ι × Π (i : ι), ι' i), ⋂ (i : ι) (H : i ∈ If.fst), s i (If.snd i))
source
theorem filter.has_basis_infi {α : Type u_1} {ι : Type u_2} {ι' : ι → Type u_3} {l : ι → filter α} {p : Π (i : ι), ι' i → Prop} {s : Π (i : ι), ι' i → set α} (hl : ∀ (i : ι), (l i).has_basis (p i) (s i)) :
(⨅ (i : ι), l i).has_basis (λ (If : Σ (I : set ι), Π (i : ↥I), ι' ↑i), If.fst.finite ∧ ∀ (i : ↥(If.fst)), p ↑i (If.snd i)) (λ (If : Σ (I : set ι), Π (i : ↥I), ι' ↑i), ⋂ (i : ↥(If.fst)), s ↑i (If.snd i))
source
theorem filter.has_basis_infi_of_directed' {α : Type u_1} {ι : Type u_2} {ι' : ι → Type u_3} [nonempty ι] {l : ι → filter α} (s : Π (i : ι), ι' i → set α) (p : Π (i : ι), ι' i → Prop) (hl : ∀ (i : ι), (l i).has_basis (p i) (s i)) (h : directed ge l) :
(⨅ (i : ι), l i).has_basis (λ (ii' : Σ (i : ι), ι' i), p ii'.fst ii'.snd) (λ (ii' : Σ (i : ι), ι' i), s ii'.fst ii'.snd)
source
theorem filter.has_basis_infi_of_directed {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [nonempty ι] {l : ι → filter α} (s : ι → ι' → set α) (p : ι → ι' → Prop) (hl : ∀ (i : ι), (l i).has_basis (p i) (s i)) (h : directed ge l) :
(⨅ (i : ι), l i).has_basis (λ (ii' : ι × ι'), p ii'.fst ii'.snd) (λ (ii' : ι × ι'), s ii'.fst ii'.snd)
source
theorem filter.has_basis_binfi_of_directed' {α : Type u_1} {ι : Type u_2} {ι' : ι → Type u_3} {dom : set ι} (hdom : dom.nonempty) {l : ι → filter α} (s : Π (i : ι), ι' i → set α) (p : Π (i : ι), ι' i → Prop) (hl : ∀ (i : ι), i ∈ dom → (l i).has_basis (p i) (s i)) (h : directed_on (l ⁻¹'o ge) dom) :
(⨅ (i : ι) (H : i ∈ dom), l i).has_basis (λ (ii' : Σ (i : ι), ι' i), ii'.fst ∈ dom ∧ p ii'.fst ii'.snd) (λ (ii' : Σ (i : ι), ι' i), s ii'.fst ii'.snd)
source
theorem filter.has_basis_binfi_of_directed {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} {dom : set ι} (hdom : dom.nonempty) {l : ι → filter α} (s : ι → ι' → set α) (p : ι → ι' → Prop) (hl : ∀ (i : ι), i ∈ dom → (l i).has_basis (p i) (s i)) (h : directed_on (l ⁻¹'o ge) dom) :
(⨅ (i : ι) (H : i ∈ dom), l i).has_basis (λ (ii' : ι × ι'), ii'.fst ∈ dom ∧ p ii'.fst ii'.snd) (λ (ii' : ι × ι'), s ii'.fst ii'.snd)
source
theorem filter.has_basis_principal {α : Type u_1} (t : set α) :
(filter.principal t).has_basis (λ (i : unit), true) (λ (i : unit), t)
source
theorem filter.has_basis_pure {α : Type u_1} (x : α) :
(has_pure.pure x).has_basis (λ (i : unit), true) (λ (i : unit), {x})
source
theorem filter.has_basis.sup' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l l' : filter α} {p : ι → Prop} {s : ι → set α} {p' : ι' → Prop} {s' : ι' → set α} (hl : l.has_basis p s) (hl' : l'.has_basis p' s') :
(l ⊔ l').has_basis (λ (i : pprod ι ι'), p i.fst ∧ p' i.snd) (λ (i : pprod ι ι'), s i.fst ∪ s' i.snd)
source
theorem filter.has_basis.sup {α : Type u_1} {l l' : filter α} {ι : Type u_2} {ι' : Type u_3} {p : ι → Prop} {s : ι → set α} {p' : ι' → Prop} {s' : ι' → set α} (hl : l.has_basis p s) (hl' : l'.has_basis p' s') :
(l ⊔ l').has_basis (λ (i : ι × ι'), p i.fst ∧ p' i.snd) (λ (i : ι × ι'), s i.fst ∪ s' i.snd)
source
theorem filter.has_basis_supr {α : Type u_1} {ι : Sort u_2} {ι' : ι → Type u_3} {l : ι → filter α} {p : Π (i : ι), ι' i → Prop} {s : Π (i : ι), ι' i → set α} (hl : ∀ (i : ι), (l i).has_basis (p i) (s i)) :
(⨆ (i : ι), l i).has_basis (λ (f : Π (i : ι), ι' i), ∀ (i : ι), p i (f i)) (λ (f : Π (i : ι), ι' i), ⋃ (i : ι), s i (f i))
source
theorem filter.has_basis.sup_principal {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} (hl : l.has_basis p s) (t : set α) :
(l ⊔ filter.principal t).has_basis p (λ (i : ι), s i ∪ t)
source
theorem filter.has_basis.sup_pure {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} (hl : l.has_basis p s) (x : α) :
(l ⊔ has_pure.pure x).has_basis p (λ (i : ι), s i ∪ {x})
source
theorem filter.has_basis.inf_principal {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} (hl : l.has_basis p s) (s' : set α) :
(l ⊓ filter.principal s').has_basis p (λ (i : ι), s i ∩ s')
source
theorem filter.has_basis.principal_inf {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} (hl : l.has_basis p s) (s' : set α) :
(filter.principal s' ⊓ l).has_basis p (λ (i : ι), s' ∩ s i)
source
theorem filter.has_basis.inf_basis_ne_bot_iff {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l l' : filter α} {p : ι → Prop} {s : ι → set α} {p' : ι' → Prop} {s' : ι' → set α} (hl : l.has_basis p s) (hl' : l'.has_basis p' s') :
(l ⊓ l').ne_bot ↔ ∀ ⦃i : ι⦄, p i → ∀ ⦃i' : ι'⦄, p' i' → (s i ∩ s' i').nonempty
source
theorem filter.has_basis.inf_ne_bot_iff {α : Type u_1} {ι : Sort u_4} {l l' : filter α} {p : ι → Prop} {s : ι → set α} (hl : l.has_basis p s) :
(l ⊓ l').ne_bot ↔ ∀ ⦃i : ι⦄, p i → ∀ ⦃s' : set α⦄, s' ∈ l' → (s i ∩ s').nonempty
source
theorem filter.has_basis.inf_principal_ne_bot_iff {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} (hl : l.has_basis p s) {t : set α} :
(l ⊓ filter.principal t).ne_bot ↔ ∀ ⦃i : ι⦄, p i → (s i ∩ t).nonempty
source
theorem filter.has_basis.disjoint_iff {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l l' : filter α} {p : ι → Prop} {s : ι → set α} {p' : ι' → Prop} {s' : ι' → set α} (hl : l.has_basis p s) (hl' : l'.has_basis p' s') :
disjoint l l' ↔ ∃ (i : ι) (hi : p i) (i' : ι') (hi' : p' i'), disjoint (s i) (s' i')
source
theorem disjoint.exists_mem_filter_basis {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l l' : filter α} {p : ι → Prop} {s : ι → set α} {p' : ι' → Prop} {s' : ι' → set α} (h : disjoint l l') (hl : l.has_basis p s) (hl' : l'.has_basis p' s') :
∃ (i : ι) (hi : p i) (i' : ι') (hi' : p' i'), disjoint (s i) (s' i')
source
theorem pairwise.exists_mem_filter_basis_of_disjoint {α : Type u_1} {I : Type u_2} [finite I] {l : I → filter α} {ι : I → Sort u_3} {p : Π (i : I), ι i → Prop} {s : Π (i : I), ι i → set α} (hd : pairwise (disjoint on l)) (h : ∀ (i : I), (l i).has_basis (p i) (s i)) :
∃ (ind : Π (i : I), ι i), (∀ (i : I), p i (ind i)) ∧ pairwise (disjoint on λ (i : I), s i (ind i))
source
theorem set.pairwise_disjoint.exists_mem_filter_basis {α : Type u_1} {I : Type u_2} {l : I → filter α} {ι : I → Sort u_3} {p : Π (i : I), ι i → Prop} {s : Π (i : I), ι i → set α} {S : set I} (hd : S.pairwise_disjoint l) (hS : S.finite) (h : ∀ (i : I), (l i).has_basis (p i) (s i)) :
∃ (ind : Π (i : I), ι i), (∀ (i : I), p i (ind i)) ∧ S.pairwise_disjoint (λ (i : I), s i (ind i))
source
theorem filter.inf_ne_bot_iff {α : Type u_1} {l l' : filter α} :
(l ⊓ l').ne_bot ↔ ∀ ⦃s : set α⦄, s ∈ l → ∀ ⦃s' : set α⦄, s' ∈ l' → (s ∩ s').nonempty
source
theorem filter.inf_principal_ne_bot_iff {α : Type u_1} {l : filter α} {s : set α} :
(l ⊓ filter.principal s).ne_bot ↔ ∀ (U : set α), U ∈ l → (U ∩ s).nonempty
source
theorem filter.mem_iff_inf_principal_compl {α : Type u_1} {f : filter α} {s : set α} :
s ∈ f ↔ f ⊓ filter.principal sᶜ = ⊥
source
theorem filter.not_mem_iff_inf_principal_compl {α : Type u_1} {f : filter α} {s : set α} :
s ∉ f ↔ (f ⊓ filter.principal sᶜ).ne_bot
source
@[simp]
theorem filter.disjoint_principal_right {α : Type u_1} {f : filter α} {s : set α} :
disjoint f (filter.principal s) ↔ sᶜ ∈ f
source
@[simp]
theorem filter.disjoint_principal_left {α : Type u_1} {f : filter α} {s : set α} :
disjoint (filter.principal s) f ↔ sᶜ ∈ f
source
@[simp]
theorem filter.disjoint_principal_principal {α : Type u_1} {s t : set α} :
disjoint (filter.principal s) (filter.principal t) ↔ disjoint s t
source
theorem disjoint.filter_principal {α : Type u_1} {s t : set α} :
disjoint s t → disjoint (filter.principal s) (filter.principal t)

Alias of the reverse direction of filter.disjoint_principal_principal.

source
@[simp]
theorem filter.disjoint_pure_pure {α : Type u_1} {x y : α} :
disjoint (has_pure.pure x) (has_pure.pure y) ↔ x ≠ y
source
@[simp]
theorem filter.compl_diagonal_mem_prod {α : Type u_1} {l₁ l₂ : filter α} :
(set.diagonal α)ᶜ ∈ l₁.prod l₂ ↔ disjoint l₁ l₂
source
theorem filter.has_basis.disjoint_iff_left {α : Type u_1} {ι : Sort u_4} {l l' : filter α} {p : ι → Prop} {s : ι → set α} (h : l.has_basis p s) :
disjoint l l' ↔ ∃ (i : ι) (hi : p i), (s i)ᶜ ∈ l'
source
theorem filter.has_basis.disjoint_iff_right {α : Type u_1} {ι : Sort u_4} {l l' : filter α} {p : ι → Prop} {s : ι → set α} (h : l.has_basis p s) :
disjoint l' l ↔ ∃ (i : ι) (hi : p i), (s i)ᶜ ∈ l'
source
theorem filter.le_iff_forall_inf_principal_compl {α : Type u_1} {f g : filter α} :
f ≤ g ↔ ∀ (V : set α), V ∈ g → f ⊓ filter.principal Vᶜ = ⊥
source
theorem filter.inf_ne_bot_iff_frequently_left {α : Type u_1} {f g : filter α} :
(f ⊓ g).ne_bot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → (∃ᶠ (x : α) in g, p x)
source
theorem filter.inf_ne_bot_iff_frequently_right {α : Type u_1} {f g : filter α} :
(f ⊓ g).ne_bot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in g, p x) → (∃ᶠ (x : α) in f, p x)
source
theorem filter.has_basis.eq_binfi {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} (h : l.has_basis p s) :
l = ⨅ (i : ι) (_x : p i), filter.principal (s i)
source
theorem filter.has_basis.eq_infi {α : Type u_1} {ι : Sort u_4} {l : filter α} {s : ι → set α} (h : l.has_basis (λ (_x : ι), true) s) :
l = ⨅ (i : ι), filter.principal (s i)
source
theorem filter.has_basis_infi_principal {α : Type u_1} {ι : Sort u_4} {s : ι → set α} (h : directed ge s) [nonempty ι] :
(⨅ (i : ι), filter.principal (s i)).has_basis (λ (_x : ι), true) s
source
theorem filter.has_basis_infi_principal_finite {α : Type u_1} {ι : Type u_2} (s : ι → set α) :
(⨅ (i : ι), filter.principal (s i)).has_basis (λ (t : set ι), t.finite) (λ (t : set ι), ⋂ (i : ι) (H : i ∈ t), s i)

If s : ι → set α is an indexed family of sets, then finite intersections of s i form a basis of ⨅ i, 𝓟 (s i).

source
theorem filter.has_basis_binfi_principal {α : Type u_1} {β : Type u_2} {s : β → set α} {S : set β} (h : directed_on (s ⁻¹'o ge) S) (ne : S.nonempty) :
(⨅ (i : β) (H : i ∈ S), filter.principal (s i)).has_basis (λ (i : β), i ∈ S) s
source
theorem filter.has_basis_binfi_principal' {α : Type u_1} {ι : Type u_2} {p : ι → Prop} {s : ι → set α} (h : ∀ (i : ι), p i → ∀ (j : ι), p j → (∃ (k : ι) (h : p k), s k ⊆ s i ∧ s k ⊆ s j)) (ne : ∃ (i : ι), p i) :
(⨅ (i : ι) (h : p i), filter.principal (s i)).has_basis p s
source
theorem filter.has_basis.map {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} (f : α → β) (hl : l.has_basis p s) :
(filter.map f l).has_basis p (λ (i : ι), f '' s i)
source
theorem filter.has_basis.comap {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} (f : β → α) (hl : l.has_basis p s) :
(filter.comap f l).has_basis p (λ (i : ι), f ⁻¹' s i)
source
theorem filter.comap_has_basis {α : Type u_1} {β : Type u_2} (f : α → β) (l : filter β) :
(filter.comap f l).has_basis (λ (s : set β), s ∈ l) (λ (s : set β), f ⁻¹' s)
source
theorem filter.has_basis.forall_mem_mem {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} (h : l.has_basis p s) {x : α} :
(∀ (t : set α), t ∈ l → x ∈ t) ↔ ∀ (i : ι), p i → x ∈ s i
source
@[protected]
theorem filter.has_basis.binfi_mem {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} [complete_lattice β] {f : set α → β} (h : l.has_basis p s) (hf : monotone f) :
(⨅ (t : set α) (H : t ∈ l), f t) = ⨅ (i : ι) (hi : p i), f (s i)
source
@[protected]
theorem filter.has_basis.bInter_mem {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} {f : set α → set β} (h : l.has_basis p s) (hf : monotone f) :
(⋂ (t : set α) (H : t ∈ l), f t) = ⋂ (i : ι) (hi : p i), f (s i)
source
theorem filter.has_basis.sInter_sets {α : Type u_1} {ι : Sort u_4} {l : filter α} {p : ι → Prop} {s : ι → set α} (h : l.has_basis p s) :
⋂₀ l.sets = ⋂ (i : ι) (hi : p i), s i
source
structure filter.is_antitone_basis {α : Type u_1} {ι'' : Type u_6} [preorder ι''] (s'' : ι'' → set α) :
Prop

is_antitone_basis s means the image of s is a filter basis such that s is decreasing.

source
structure filter.has_antitone_basis {α : Type u_1} {ι'' : Type u_6} [preorder ι''] (l : filter α) (s : ι'' → set α) :
Prop

We say that a filter l has an antitone basis s : ι → set α, if t ∈ l if and only if t includes s i for some i, and s is decreasing.

source
theorem filter.has_antitone_basis.map {α : Type u_1} {β : Type u_2} {ι'' : Type u_6} [preorder ι''] {l : filter α} {s : ι'' → set α} {m : α → β} (hf : l.has_antitone_basis s) :
(filter.map m l).has_antitone_basis (λ (n : ι''), m '' s n)
source
theorem filter.has_basis.tendsto_left_iff {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {la : filter α} {pa : ι → Prop} {sa : ι → set α} {lb : filter β} {f : α → β} (hla : la.has_basis pa sa) :
filter.tendsto f la lb ↔ ∀ (t : set β), t ∈ lb → (∃ (i : ι) (hi : pa i), set.maps_to f (sa i) t)
source
theorem filter.has_basis.tendsto_right_iff {α : Type u_1} {β : Type u_2} {ι' : Sort u_5} {la : filter α} {lb : filter β} {pb : ι' → Prop} {sb : ι' → set β} {f : α → β} (hlb : lb.has_basis pb sb) :
filter.tendsto f la lb ↔ ∀ (i : ι'), pb i → (∀ᶠ (x : α) in la, f x ∈ sb i)
source
theorem filter.has_basis.tendsto_iff {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {ι' : Sort u_5} {la : filter α} {pa : ι → Prop} {sa : ι → set α} {lb : filter β} {pb : ι' → Prop} {sb : ι' → set β} {f : α → β} (hla : la.has_basis pa sa) (hlb : lb.has_basis pb sb) :
filter.tendsto f la lb ↔ ∀ (ib : ι'), pb ib → (∃ (ia : ι) (hia : pa ia), ∀ (x : α), x ∈ sa ia → f x ∈ sb ib)
source
theorem filter.tendsto.basis_left {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {la : filter α} {pa : ι → Prop} {sa : ι → set α} {lb : filter β} {f : α → β} (H : filter.tendsto f la lb) (hla : la.has_basis pa sa) (t : set β) (H_1 : t ∈ lb) :
∃ (i : ι) (hi : pa i), set.maps_to f (sa i) t
source
theorem filter.tendsto.basis_right {α : Type u_1} {β : Type u_2} {ι' : Sort u_5} {la : filter α} {lb : filter β} {pb : ι' → Prop} {sb : ι' → set β} {f : α → β} (H : filter.tendsto f la lb) (hlb : lb.has_basis pb sb) (i : ι') (hi : pb i) :
∀ᶠ (x : α) in la, f x ∈ sb i
source
theorem filter.tendsto.basis_both {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {ι' : Sort u_5} {la : filter α} {pa : ι → Prop} {sa : ι → set α} {lb : filter β} {pb : ι' → Prop} {sb : ι' → set β} {f : α → β} (H : filter.tendsto f la lb) (hla : la.has_basis pa sa) (hlb : lb.has_basis pb sb) (ib : ι') (hib : pb ib) :
∃ (ia : ι) (hia : pa ia), ∀ (x : α), x ∈ sa ia → f x ∈ sb ib
source
theorem filter.has_basis.prod_pprod {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {ι' : Sort u_5} {la : filter α} {pa : ι → Prop} {sa : ι → set α} {lb : filter β} {pb : ι' → Prop} {sb : ι' → set β} (hla : la.has_basis pa sa) (hlb : lb.has_basis pb sb) :
(la.prod lb).has_basis (λ (i : pprod ι ι'), pa i.fst ∧ pb i.snd) (λ (i : pprod ι ι'), sa i.fst ×ˢ sb i.snd)
source
theorem filter.has_basis.prod {α : Type u_1} {β : Type u_2} {la : filter α} {lb : filter β} {ι : Type u_3} {ι' : Type u_4} {pa : ι → Prop} {sa : ι → set α} {pb : ι' → Prop} {sb : ι' → set β} (hla : la.has_basis pa sa) (hlb : lb.has_basis pb sb) :
(la.prod lb).has_basis (λ (i : ι × ι'), pa i.fst ∧ pb i.snd) (λ (i : ι × ι'), sa i.fst ×ˢ sb i.snd)
source
theorem filter.has_basis.prod_same_index {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {la : filter α} {sa : ι → set α} {lb : filter β} {p : ι → Prop} {sb : ι → set β} (hla : la.has_basis p sa) (hlb : lb.has_basis p sb) (h_dir : ∀ {i j : ι}, p i → p j → (∃ (k : ι), p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j)) :
(la.prod lb).has_basis p (λ (i : ι), sa i ×ˢ sb i)
source
theorem filter.has_basis.prod_same_index_mono {α : Type u_1} {β : Type u_2} {la : filter α} {lb : filter β} {ι : Type u_3} [linear_order ι] {p : ι → Prop} {sa : ι → set α} {sb : ι → set β} (hla : la.has_basis p sa) (hlb : lb.has_basis p sb) (hsa : monotone_on sa {i : ι | p i}) (hsb : monotone_on sb {i : ι | p i}) :
(la.prod lb).has_basis p (λ (i : ι), sa i ×ˢ sb i)
source
theorem filter.has_basis.prod_same_index_anti {α : Type u_1} {β : Type u_2} {la : filter α} {lb : filter β} {ι : Type u_3} [linear_order ι] {p : ι → Prop} {sa : ι → set α} {sb : ι → set β} (hla : la.has_basis p sa) (hlb : lb.has_basis p sb) (hsa : antitone_on sa {i : ι | p i}) (hsb : antitone_on sb {i : ι | p i}) :
(la.prod lb).has_basis p (λ (i : ι), sa i ×ˢ sb i)
source
theorem filter.has_basis.prod_self {α : Type u_1} {ι : Sort u_4} {la : filter α} {pa : ι → Prop} {sa : ι → set α} (hl : la.has_basis pa sa) :
(la.prod la).has_basis pa (λ (i : ι), sa i ×ˢ sa i)
source
theorem filter.mem_prod_self_iff {α : Type u_1} {la : filter α} {s : set (α × α)} :
s ∈ la.prod la ↔ ∃ (t : set α) (H : t ∈ la), t ×ˢ t ⊆ s
source
theorem filter.has_antitone_basis.prod {α : Type u_1} {β : Type u_2} {ι : Type u_3} [linear_order ι] {f : filter α} {g : filter β} {s : ι → set α} {t : ι → set β} (hf : f.has_antitone_basis s) (hg : g.has_antitone_basis t) :
(f.prod g).has_antitone_basis (λ (n : ι), s n ×ˢ t n)
source
theorem filter.has_basis.coprod {α : Type u_1} {β : Type u_2} {la : filter α} {lb : filter β} {ι : Type u_3} {ι' : Type u_4} {pa : ι → Prop} {sa : ι → set α} {pb : ι' → Prop} {sb : ι' → set β} (hla : la.has_basis pa sa) (hlb : lb.has_basis pb sb) :
(la.coprod lb).has_basis (λ (i : ι × ι'), pa i.fst ∧ pb i.snd) (λ (i : ι × ι'), prod.fst ⁻¹' sa i.fst ∪ prod.snd ⁻¹' sb i.snd)
source
theorem filter.map_sigma_mk_comap {α : Type u_1} {β : Type u_2} {π : α → Type u_3} {π' : β → Type u_4} {f : α → β} (hf : function.injective f) (g : Π (a : α), π a → π' (f a)) (a : α) (l : filter (π' (f a))) :
filter.map (sigma.mk a) (filter.comap (g a) l) = filter.comap (sigma.map f g) (filter.map (sigma.mk (f a)) l)
source
@[class]
structure filter.is_countably_generated {α : Type u_1} (f : filter α) :
Prop

is_countably_generated f means f = generate s for some countable s.

Instances of this typeclass
source
structure filter.is_countable_basis {α : Type u_1} {ι : Type u_4} (p : ι → Prop) (s : ι → set α) :
Prop

is_countable_basis p s means the image of s bounded by p is a countable filter basis.

source
structure filter.has_countable_basis {α : Type u_1} {ι : Type u_4} (l : filter α) (p : ι → Prop) (s : ι → set α) :
Prop

We say that a filter l has a countable basis s : ι → set α bounded by p : ι → Prop, if t ∈ l if and only if t includes s i for some i such that p i, and the set defined by p is countable.

source
structure filter.countable_filter_basis (α : Type u_6) :
Type u_6

A countable filter basis B on a type α is a nonempty countable collection of sets of α such that the intersection of two elements of this collection contains some element of the collection.

Instances for filter.countable_filter_basis
source
@[protected, instance]
def filter.nat.inhabited_countable_filter_basis  :
inhabited (filter.countable_filter_basis ℕ)
Equations
source
theorem filter.has_countable_basis.is_countably_generated {α : Type u_1} {ι : Type u_4} {f : filter α} {p : ι → Prop} {s : ι → set α} (h : f.has_countable_basis p s) :
f.is_countably_generated
source
theorem filter.antitone_seq_of_seq {α : Type u_1} (s : ℕ → set α) :
∃ (t : ℕ → set α), antitone t ∧ (⨅ (i : ℕ), filter.principal (s i)) = ⨅ (i : ℕ), filter.principal (t i)
source
theorem filter.countable_binfi_eq_infi_seq {α : Type u_1} {ι : Type u_4} [complete_lattice α] {B : set ι} (Bcbl : B.countable) (Bne : B.nonempty) (f : ι → α) :
∃ (x : ℕ → ι), (⨅ (t : ι) (H : t ∈ B), f t) = ⨅ (i : ℕ), f (x i)
source
theorem filter.countable_binfi_eq_infi_seq' {α : Type u_1} {ι : Type u_4} [complete_lattice α] {B : set ι} (Bcbl : B.countable) (f : ι → α) {i₀ : ι} (h : f i₀ = ⊤) :
∃ (x : ℕ → ι), (⨅ (t : ι) (H : t ∈ B), f t) = ⨅ (i : ℕ), f (x i)
source
theorem filter.countable_binfi_principal_eq_seq_infi {α : Type u_1} {B : set (set α)} (Bcbl : B.countable) :
∃ (x : ℕ → set α), (⨅ (t : set α) (H : t ∈ B), filter.principal t) = ⨅ (i : ℕ), filter.principal (x i)
source
@[protected]
theorem filter.has_antitone_basis.mem_iff {α : Type u_1} {ι : Type u_4} [preorder ι] {l : filter α} {s : ι → set α} (hs : l.has_antitone_basis s) {t : set α} :
t ∈ l ↔ ∃ (i : ι), s i ⊆ t
source
@[protected]
theorem filter.has_antitone_basis.mem {α : Type u_1} {ι : Type u_4} [preorder ι] {l : filter α} {s : ι → set α} (hs : l.has_antitone_basis s) (i : ι) :
s i ∈ l
source
theorem filter.has_antitone_basis.has_basis_ge {α : Type u_1} {ι : Type u_4} [preorder ι] [is_directed ι has_le.le] {l : filter α} {s : ι → set α} (hs : l.has_antitone_basis s) (i : ι) :
l.has_basis (λ (j : ι), i ≤ j) s
source
theorem filter.has_basis.exists_antitone_subbasis {α : Type u_1} {ι' : Sort u_5} {f : filter α} [h : f.is_countably_generated] {p : ι' → Prop} {s : ι' → set α} (hs : f.has_basis p s) :
∃ (x : ℕ → ι'), (∀ (i : ℕ), p (x i)) ∧ f.has_antitone_basis (λ (i : ℕ), s (x i))

If f is countably generated and f.has_basis p s, then f admits a decreasing basis enumerated by natural numbers such that all sets have the form s i. More precisely, there is a sequence i n such that p (i n) for all n and s (i n) is a decreasing sequence of sets which forms a basis of f

source
theorem filter.exists_antitone_basis {α : Type u_1} (f : filter α) [f.is_countably_generated] :
∃ (x : ℕ → set α), f.has_antitone_basis x

A countably generated filter admits a basis formed by an antitone sequence of sets.

source
theorem filter.exists_antitone_seq {α : Type u_1} (f : filter α) [f.is_countably_generated] :
∃ (x : ℕ → set α), antitone x ∧ ∀ {s : set α}, s ∈ f ↔ ∃ (i : ℕ), x i ⊆ s
source
@[protected, instance]
def filter.inf.is_countably_generated {α : Type u_1} (f g : filter α) [f.is_countably_generated] [g.is_countably_generated] :
(f ⊓ g).is_countably_generated
source
@[protected, instance]
def filter.map.is_countably_generated {α : Type u_1} {β : Type u_2} (l : filter α) [l.is_countably_generated] (f : α → β) :
(filter.map f l).is_countably_generated
source
@[protected, instance]
def filter.comap.is_countably_generated {α : Type u_1} {β : Type u_2} (l : filter β) [l.is_countably_generated] (f : α → β) :
(filter.comap f l).is_countably_generated
source
@[protected, instance]
def filter.sup.is_countably_generated {α : Type u_1} (f g : filter α) [f.is_countably_generated] [g.is_countably_generated] :
(f ⊔ g).is_countably_generated
source
@[protected, instance]
def filter.prod.is_countably_generated {α : Type u_1} {β : Type u_2} (la : filter α) (lb : filter β) [la.is_countably_generated] [lb.is_countably_generated] :
(la.prod lb).is_countably_generated
source
@[protected, instance]
def filter.coprod.is_countably_generated {α : Type u_1} {β : Type u_2} (la : filter α) (lb : filter β) [la.is_countably_generated] [lb.is_countably_generated] :
(la.coprod lb).is_countably_generated
source
theorem filter.is_countably_generated_seq {α : Type u_1} {β : Type u_2} [countable β] (x : β → set α) :
(⨅ (i : β), filter.principal (x i)).is_countably_generated
source
theorem filter.is_countably_generated_of_seq {α : Type u_1} {f : filter α} (h : ∃ (x : ℕ → set α), f = ⨅ (i : ℕ), filter.principal (x i)) :
f.is_countably_generated
source
theorem filter.is_countably_generated_binfi_principal {α : Type u_1} {B : set (set α)} (h : B.countable) :
(⨅ (s : set α) (H : s ∈ B), filter.principal s).is_countably_generated
source
theorem filter.is_countably_generated_iff_exists_antitone_basis {α : Type u_1} {f : filter α} :
f.is_countably_generated ↔ ∃ (x : ℕ → set α), f.has_antitone_basis x
source
@[instance]
theorem filter.is_countably_generated_principal {α : Type u_1} (s : set α) :
(filter.principal s).is_countably_generated
source
@[instance]
theorem filter.is_countably_generated_pure {α : Type u_1} (a : α) :
(has_pure.pure a).is_countably_generated
source
@[instance]
theorem filter.is_countably_generated_bot {α : Type u_1} :
⊥.is_countably_generated
source
@[instance]
theorem filter.is_countably_generated_top {α : Type u_1} :
⊤.is_countably_generated
source
@[protected, instance]
def filter.infi.is_countably_generated {α : Type u_1} {ι : Sort u_2} [countable ι] (f : ι → filter α) [∀ (i : ι), (f i).is_countably_generated] :
(⨅ (i : ι), f i).is_countably_generated