Filter bases

A filter basis B : FilterBasis α 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.IsBasis p s makes sure the range of s bounded by p (ie. s '' setOf p) defines a filter basis h.filterBasis.

If one already has a filter l on α, Filter.HasBasis 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.IsBasis p s, and l = h.filterBasis.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 HasBasis.index (h : Filter.HasBasis 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.IsCountablyGenerated means there is a countable set of sets which generates s. This is reformulated in term of bases, and consequences are derived.

Main statements

• Filter.HasBasis.mem_iff, HasBasis.mem_of_superset, HasBasis.mem_of_mem : restate t ∈ f in terms of a basis;

• Filter.basis_sets : all sets of a filter form a basis;

• Filter.HasBasis.inf, Filter.HasBasis.inf_principal, Filter.HasBasis.prod, Filter.HasBasis.prod_self, Filter.HasBasis.map, Filter.HasBasis.comap : combinators to construct filters of l ⊓ l', l ⊓ 𝓟 t, l ×ˢ l', l ×ˢ l, l.map f, l.comap f respectively;

• Filter.HasBasis.le_iff, Filter.HasBasis.ge_iff, Filter.HasBasis.le_basis_iff : restate l ≤ l' in terms of bases.

• Filter.HasBasis.tendsto_right_iff, Filter.HasBasis.tendsto_left_iff, Filter.HasBasis.tendsto_iff : restate Tendsto f l l' in terms of bases.

• isCountablyGenerated_iff_exists_antitone_basis : proves a filter is countably generated if and only if it admits a basis parametrized by a decreasing sequence of sets indexed by ℕ.

• tendsto_iff_seq_tendsto : an abstract version of "sequentially continuous implies continuous".

Implementation notes

As with Set.iUnion/biUnion/Set.sUnion, there are three different approaches to filter bases:

• Filter.HasBasis l s, s : Set (Set α);
• Filter.HasBasis l s, s : ι → Set α;
• Filter.HasBasis l p s, p : ι → Prop, s : ι → Set α.

We use the latter one because, e.g., 𝓝 x in an EMetricSpace or in a MetricSpace has a basis of this form. The other two can be emulated using s = id or p = fun _ ↦ True.

With this approach sometimes one needs to simp the statement provided by the Filter.HasBasis machinery, e.g., simp only [true_and] or simp only [forall_const] can help with the case p = fun _ ↦ True.

structure FilterBasis (α : Type u_6) : Type u_6

• sets : Set (Set α)

  Sets of a filter basis.

• nonempty : Set.Nonempty s.sets

  The set of filter basis sets is nonempty.

• inter_sets : ∀ {x y : Set α}, x ∈ s.sets → y ∈ s.sets → ∃ z, z ∈ s.sets ∧ z ⊆ x ∩ y

  The set of filter basis sets is directed downwards.

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.

instance FilterBasis.nonempty_sets {α : Type u_1} (B : FilterBasis α) : Nonempty ↑B.sets

Equations

• @FilterBasis.nonempty_sets = @FilterBasis.nonempty_sets.proof_1

instance instMembershipSetFilterBasis {α : Type u_6} : Membership (Set α) (FilterBasis α)

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

Equations

• instMembershipSetFilterBasis = { mem := fun U B => U ∈ B.sets }

@[simp]

theorem FilterBasis.mem_sets {α : Type u_1} {s : Set α} {B : FilterBasis α} : s ∈ B.sets ↔ s ∈ B

instance instInhabitedFilterBasisNat : Inhabited (FilterBasis ℕ)

Equations

• instInhabitedFilterBasisNat = { default := { sets := Set.range Set.Ici, nonempty := instInhabitedFilterBasisNat.proof_1, inter_sets := @instInhabitedFilterBasisNat.proof_2 } }

def Filter.asBasis {α : Type u_1} (f : Filter α) : FilterBasis α

View a filter as a filter basis.

Equations

• Filter.asBasis f = { sets := f.sets, nonempty := (_ : ∃ x, x ∈ f.sets), inter_sets := (_ : ∀ {x y : Set α}, x ∈ f.sets → y ∈ f.sets → ∃ z, z ∈ f.sets ∧ z ⊆ x ∩ y) }

structure Filter.IsBasis {α : Type u_1} {ι : Sort u_4} (p : ι → Prop) (s : ι → Set α) : Prop

• nonempty : ∃ i, p i

  There exists at least one i that satisfies p.

• inter : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ s✝ k ⊆ s✝ i ∩ s✝ j

  s is directed downwards on i such that p i.

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

def Filter.IsBasis.filterBasis {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → Set α} (h : Filter.IsBasis p s) : FilterBasis α

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

Equations

• One or more equations did not get rendered due to their size.

theorem Filter.IsBasis.mem_filterBasis_iff {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → Set α} (h : Filter.IsBasis p s) {U : Set α} : U ∈ Filter.IsBasis.filterBasis h ↔ ∃ i, p i ∧ s i = U

def FilterBasis.filter {α : Type u_1} (B : FilterBasis α) : Filter α

The filter associated to a filter basis.

Equations

• One or more equations did not get rendered due to their size.

theorem FilterBasis.mem_filter_iff {α : Type u_1} (B : FilterBasis α) {U : Set α} : U ∈ FilterBasis.filter B ↔ ∃ s, s ∈ B ∧ s ⊆ U

theorem FilterBasis.mem_filter_of_mem {α : Type u_1} (B : FilterBasis α) {U : Set α} : U ∈ B → U ∈ FilterBasis.filter B

theorem FilterBasis.eq_iInf_principal {α : Type u_1} (B : FilterBasis α) : FilterBasis.filter B = ⨅ (s : ↑B.sets), Filter.principal ↑s

theorem FilterBasis.generate {α : Type u_1} (B : FilterBasis α) : Filter.generate B.sets = FilterBasis.filter B

def Filter.IsBasis.filter {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → Set α} (h : Filter.IsBasis p s) : Filter α

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

Equations

• Filter.IsBasis.filter h = FilterBasis.filter (Filter.IsBasis.filterBasis h)

theorem Filter.IsBasis.mem_filter_iff {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → Set α} (h : Filter.IsBasis p s) {U : Set α} : U ∈ Filter.IsBasis.filter h ↔ ∃ i, p i ∧ s i ⊆ U

theorem Filter.IsBasis.filter_eq_generate {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → Set α} (h : Filter.IsBasis p s) : Filter.IsBasis.filter h = Filter.generate {U | ∃ i, p i ∧ s i = U}

structure Filter.HasBasis {α : Type u_1} {ι : Sort u_4} (l : Filter α) (p : ι → Prop) (s : ι → Set α) : Prop

• mem_iff' : ∀ (t : Set α), t ∈ l ↔ ∃ i, p i ∧ s✝ i ⊆ t

  A set t belongs to a filter l iff it includes an element of the basis.

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.

theorem Filter.hasBasis_generate {α : Type u_1} (s : Set (Set α)) : Filter.HasBasis (Filter.generate s) (fun t => Set.Finite t ∧ t ⊆ s) fun t => ⋂₀ t

def Filter.FilterBasis.ofSets {α : Type u_1} (s : Set (Set α)) : FilterBasis α

The smallest filter basis containing a given collection of sets.

Equations

• One or more equations did not get rendered due to their size.

theorem Filter.FilterBasis.ofSets_sets {α : Type u_1} (s : Set (Set α)) : (Filter.FilterBasis.ofSets s).sets = Set.sInter '' {t | Set.Finite t ∧ t ⊆ s}

theorem Filter.HasBasis.mem_iff {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {t : Set α} (hl : Filter.HasBasis l p s) : t ∈ l ↔ ∃ i, p i ∧ s i ⊆ t

Definition of HasBasis unfolded with implicit set argument.

theorem Filter.HasBasis.eq_of_same_basis {α : Type u_1} {ι : Sort u_4} {l : Filter α} {l' : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) (hl' : Filter.HasBasis l' p s) : l = l'

theorem Filter.hasBasis_iff {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} : Filter.HasBasis l p s ↔ ∀ (t : Set α), t ∈ l ↔ ∃ i, p i ∧ s i ⊆ t

theorem Filter.HasBasis.ex_mem {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) : ∃ i, p i

theorem Filter.HasBasis.nonempty {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) : Nonempty ι

theorem Filter.IsBasis.hasBasis {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → Set α} (h : Filter.IsBasis p s) : Filter.HasBasis (Filter.IsBasis.filter h) p s

theorem Filter.HasBasis.mem_of_superset {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {t : Set α} {i : ι} (hl : Filter.HasBasis l p s) (hi : p i) (ht : s i ⊆ t) : t ∈ l

theorem Filter.HasBasis.mem_of_mem {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {i : ι} (hl : Filter.HasBasis l p s) (hi : p i) : s i ∈ l

noncomputable def Filter.HasBasis.index {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l 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

• Filter.HasBasis.index h t ht = { val := Exists.choose (_ : ∃ i, p i ∧ s i ⊆ t), property := Filter.HasBasis.index.proof_2 h t ht }

theorem Filter.HasBasis.property_index {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {t : Set α} (h : Filter.HasBasis l p s) (ht : t ∈ l) : p ↑(Filter.HasBasis.index h t ht)

theorem Filter.HasBasis.set_index_mem {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {t : Set α} (h : Filter.HasBasis l p s) (ht : t ∈ l) : s ↑(Filter.HasBasis.index h t ht) ∈ l

theorem Filter.HasBasis.set_index_subset {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {t : Set α} (h : Filter.HasBasis l p s) (ht : t ∈ l) : s ↑(Filter.HasBasis.index h t ht) ⊆ t

theorem Filter.HasBasis.isBasis {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) : Filter.IsBasis p s

theorem Filter.HasBasis.filter_eq {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) : Filter.IsBasis.filter (_ : Filter.IsBasis p s) = l

theorem Filter.HasBasis.eq_generate {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) : l = Filter.generate {U | ∃ i, p i ∧ s i = U}

theorem Filter.generate_eq_generate_inter {α : Type u_1} (s : Set (Set α)) : Filter.generate s = Filter.generate (Set.sInter '' {t | Set.Finite t ∧ t ⊆ s})

theorem Filter.ofSets_filter_eq_generate {α : Type u_1} (s : Set (Set α)) : FilterBasis.filter (Filter.FilterBasis.ofSets s) = Filter.generate s

theorem FilterBasis.hasBasis {α : Type u_1} (B : FilterBasis α) : Filter.HasBasis (FilterBasis.filter B) (fun s => s ∈ B) id

theorem Filter.HasBasis.to_hasBasis' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (hl : Filter.HasBasis l p s) (h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i) (h' : ∀ (i' : ι'), p' i' → s' i' ∈ l) : Filter.HasBasis l p' s'

theorem Filter.HasBasis.to_hasBasis {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (hl : Filter.HasBasis l p s) (h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i) (h' : ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i') : Filter.HasBasis l p' s'

theorem Filter.HasBasis.to_subset {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) {t : ι → Set α} (h : ∀ (i : ι), p i → t i ⊆ s i) (ht : ∀ (i : ι), p i → t i ∈ l) : Filter.HasBasis l p t

theorem Filter.HasBasis.eventually_iff {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) {q : α → Prop} : (∀ᶠ (x : α) in l, q x) ↔ ∃ i, p i ∧ (⦃x : α⦄ → x ∈ s i → q x)

theorem Filter.HasBasis.frequently_iff {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) {q : α → Prop} : (∃ᶠ (x : α) in l, q x) ↔ ∀ (i : ι), p i → ∃ x, x ∈ s i ∧ q x

theorem Filter.HasBasis.exists_iff {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) {P : Set α → Prop} (mono : ⦃s t : Set α⦄ → s ⊆ t → P t → P s) : (∃ s, s ∈ l ∧ P s) ↔ ∃ i, p i ∧ P (s i)

theorem Filter.HasBasis.forall_iff {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l 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)

theorem Filter.HasBasis.neBot_iff {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) : Filter.NeBot l ↔ ∀ {i : ι}, p i → Set.Nonempty (s i)

theorem Filter.HasBasis.eq_bot_iff {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) : l = ⊥ ↔ ∃ i, p i ∧ s i = ∅

theorem Filter.generate_neBot_iff {α : Type u_1} {s : Set (Set α)} : Filter.NeBot (Filter.generate s) ↔ ∀ (t : Set (Set α)), t ⊆ s → Set.Finite t → Set.Nonempty (⋂₀ t)

theorem Filter.basis_sets {α : Type u_1} (l : Filter α) : Filter.HasBasis l (fun s => s ∈ l) id

theorem Filter.asBasis_filter {α : Type u_1} (f : Filter α) : FilterBasis.filter (Filter.asBasis f) = f

theorem Filter.hasBasis_self {α : Type u_1} {l : Filter α} {P : Set α → Prop} : Filter.HasBasis l (fun s => s ∈ l ∧ P s) id ↔ ∀ (t : Set α), t ∈ l → ∃ r, r ∈ l ∧ P r ∧ r ⊆ t

theorem Filter.HasBasis.comp_surjective {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) {g : ι' → ι} (hg : Function.Surjective g) : Filter.HasBasis l (p ∘ g) (s ∘ g)

theorem Filter.HasBasis.comp_equiv {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) (e : ι' ≃ ι) : Filter.HasBasis l (p ∘ ↑e) (s ∘ ↑e)

theorem Filter.HasBasis.restrict {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) {q : ι → Prop} (hq : ∀ (i : ι), p i → ∃ j, p j ∧ q j ∧ s j ⊆ s i) : Filter.HasBasis l (fun 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.

theorem Filter.HasBasis.restrict_subset {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) {V : Set α} (hV : V ∈ l) : Filter.HasBasis l (fun 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.

theorem Filter.HasBasis.hasBasis_self_subset {α : Type u_1} {l : Filter α} {p : Set α → Prop} (h : Filter.HasBasis l (fun s => s ∈ l ∧ p s) id) {V : Set α} (hV : V ∈ l) : Filter.HasBasis l (fun s => s ∈ l ∧ p s ∧ s ⊆ V) id

theorem Filter.HasBasis.ge_iff {α : Type u_1} {ι' : Sort u_5} {l : Filter α} {l' : Filter α} {p' : ι' → Prop} {s' : ι' → Set α} (hl' : Filter.HasBasis l' p' s') : l ≤ l' ↔ ∀ (i' : ι'), p' i' → s' i' ∈ l

theorem Filter.HasBasis.le_iff {α : Type u_1} {ι : Sort u_4} {l : Filter α} {l' : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) : l ≤ l' ↔ ∀ (t : Set α), t ∈ l' → ∃ i, p i ∧ s i ⊆ t

theorem Filter.HasBasis.le_basis_iff {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l : Filter α} {l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (hl : Filter.HasBasis l p s) (hl' : Filter.HasBasis l' p' s') : l ≤ l' ↔ ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'

theorem Filter.HasBasis.ext {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l : Filter α} {l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (hl : Filter.HasBasis l p s) (hl' : Filter.HasBasis l' 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'

theorem Filter.HasBasis.inf' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l : Filter α} {l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (hl : Filter.HasBasis l p s) (hl' : Filter.HasBasis l' p' s') : Filter.HasBasis (l ⊓ l') (fun i => p i.fst ∧ p' i.snd) fun i => s i.fst ∩ s' i.snd

theorem Filter.HasBasis.inf {α : Type u_1} {l : Filter α} {l' : Filter α} {ι : Type u_6} {ι' : Type u_7} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (hl : Filter.HasBasis l p s) (hl' : Filter.HasBasis l' p' s') : Filter.HasBasis (l ⊓ l') (fun i => p i.fst ∧ p' i.snd) fun i => s i.fst ∩ s' i.snd

theorem Filter.hasBasis_iInf' {α : Type u_1} {ι : Type u_6} {ι' : ι → Type u_7} {l : ι → Filter α} {p : (i : ι) → ι' i → Prop} {s : (i : ι) → ι' i → Set α} (hl : ∀ (i : ι), Filter.HasBasis (l i) (p i) (s i)) : Filter.HasBasis (⨅ (i : ι), l i) (fun If => Set.Finite If.fst ∧ ((i : ι) → i ∈ If.fst → p i (Prod.snd (Set ι) ((i : ι) → ι' i) If i))) fun If => ⋂ (i : ι) (_ : i ∈ If.fst), s i (Prod.snd (Set ι) ((i : ι) → ι' i) If i)

theorem Filter.hasBasis_iInf {α : Type u_1} {ι : Type u_6} {ι' : ι → Type u_7} {l : ι → Filter α} {p : (i : ι) → ι' i → Prop} {s : (i : ι) → ι' i → Set α} (hl : ∀ (i : ι), Filter.HasBasis (l i) (p i) (s i)) : Filter.HasBasis (⨅ (i : ι), l i) (fun If => Set.Finite If.fst ∧ ((i : ↑If.fst) → p (↑i) (Sigma.snd (Set ι) (fun I => (i : ↑I) → ι' ↑i) If i))) fun If => ⋂ (i : ↑If.fst), s (↑i) (Sigma.snd (Set ι) (fun I => (i : ↑I) → ι' ↑i) If i)

theorem Filter.hasBasis_iInf_of_directed' {α : Type u_1} {ι : Type u_6} {ι' : ι → Type u_7} [Nonempty ι] {l : ι → Filter α} (s : (i : ι) → ι' i → Set α) (p : (i : ι) → ι' i → Prop) (hl : ∀ (i : ι), Filter.HasBasis (l i) (p i) (s i)) (h : Directed (fun x x_1 => x ≥ x_1) l) : Filter.HasBasis (⨅ (i : ι), l i) (fun ii' => p ii'.fst ii'.snd) fun ii' => s ii'.fst ii'.snd

theorem Filter.hasBasis_iInf_of_directed {α : Type u_1} {ι : Type u_6} {ι' : Type u_7} [Nonempty ι] {l : ι → Filter α} (s : ι → ι' → Set α) (p : ι → ι' → Prop) (hl : ∀ (i : ι), Filter.HasBasis (l i) (p i) (s i)) (h : Directed (fun x x_1 => x ≥ x_1) l) : Filter.HasBasis (⨅ (i : ι), l i) (fun ii' => p ii'.fst ii'.snd) fun ii' => s ii'.fst ii'.snd

theorem Filter.hasBasis_biInf_of_directed' {α : Type u_1} {ι : Type u_6} {ι' : ι → Type u_7} {dom : Set ι} (hdom : Set.Nonempty dom) {l : ι → Filter α} (s : (i : ι) → ι' i → Set α) (p : (i : ι) → ι' i → Prop) (hl : ∀ (i : ι), i ∈ dom → Filter.HasBasis (l i) (p i) (s i)) (h : DirectedOn (l ⁻¹'o GE.ge) dom) : Filter.HasBasis (⨅ (i : ι) (_ : i ∈ dom), l i) (fun ii' => ii'.fst ∈ dom ∧ p ii'.fst ii'.snd) fun ii' => s ii'.fst ii'.snd

theorem Filter.hasBasis_biInf_of_directed {α : Type u_1} {ι : Type u_6} {ι' : Type u_7} {dom : Set ι} (hdom : Set.Nonempty dom) {l : ι → Filter α} (s : ι → ι' → Set α) (p : ι → ι' → Prop) (hl : ∀ (i : ι), i ∈ dom → Filter.HasBasis (l i) (p i) (s i)) (h : DirectedOn (l ⁻¹'o GE.ge) dom) : Filter.HasBasis (⨅ (i : ι) (_ : i ∈ dom), l i) (fun ii' => ii'.fst ∈ dom ∧ p ii'.fst ii'.snd) fun ii' => s ii'.fst ii'.snd

theorem Filter.hasBasis_principal {α : Type u_1} (t : Set α) : Filter.HasBasis (Filter.principal t) (fun x => True) fun x => t

theorem Filter.hasBasis_pure {α : Type u_1} (x : α) : Filter.HasBasis (pure x) (fun x => True) fun x => {x}

theorem Filter.HasBasis.sup' {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l : Filter α} {l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (hl : Filter.HasBasis l p s) (hl' : Filter.HasBasis l' p' s') : Filter.HasBasis (l ⊔ l') (fun i => p i.fst ∧ p' i.snd) fun i => s i.fst ∪ s' i.snd

theorem Filter.HasBasis.sup {α : Type u_1} {l : Filter α} {l' : Filter α} {ι : Type u_6} {ι' : Type u_7} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (hl : Filter.HasBasis l p s) (hl' : Filter.HasBasis l' p' s') : Filter.HasBasis (l ⊔ l') (fun i => p i.fst ∧ p' i.snd) fun i => s i.fst ∪ s' i.snd

theorem Filter.hasBasis_iSup {α : Type u_1} {ι : Sort u_6} {ι' : ι → Type u_7} {l : ι → Filter α} {p : (i : ι) → ι' i → Prop} {s : (i : ι) → ι' i → Set α} (hl : ∀ (i : ι), Filter.HasBasis (l i) (p i) (s i)) : Filter.HasBasis (⨆ (i : ι), l i) (fun f => (i : ι) → p i (f i)) fun f => ⋃ (i : ι), s i (f i)

theorem Filter.HasBasis.sup_principal {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) (t : Set α) : Filter.HasBasis (l ⊔ Filter.principal t) p fun i => s i ∪ t

theorem Filter.HasBasis.sup_pure {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) (x : α) : Filter.HasBasis (l ⊔ pure x) p fun i => s i ∪ {x}

theorem Filter.HasBasis.inf_principal {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) (s' : Set α) : Filter.HasBasis (l ⊓ Filter.principal s') p fun i => s i ∩ s'

theorem Filter.HasBasis.principal_inf {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) (s' : Set α) : Filter.HasBasis (Filter.principal s' ⊓ l) p fun i => s' ∩ s i

theorem Filter.HasBasis.inf_basis_neBot_iff {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l : Filter α} {l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (hl : Filter.HasBasis l p s) (hl' : Filter.HasBasis l' p' s') : Filter.NeBot (l ⊓ l') ↔ ∀ ⦃i : ι⦄, p i → ∀ ⦃i' : ι'⦄, p' i' → Set.Nonempty (s i ∩ s' i')

theorem Filter.HasBasis.inf_neBot_iff {α : Type u_1} {ι : Sort u_4} {l : Filter α} {l' : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) : Filter.NeBot (l ⊓ l') ↔ ∀ ⦃i : ι⦄, p i → ∀ ⦃s' : Set α⦄, s' ∈ l' → Set.Nonempty (s i ∩ s')

theorem Filter.HasBasis.inf_principal_neBot_iff {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (hl : Filter.HasBasis l p s) {t : Set α} : Filter.NeBot (l ⊓ Filter.principal t) ↔ ∀ ⦃i : ι⦄, p i → Set.Nonempty (s i ∩ t)

theorem Filter.HasBasis.disjoint_iff {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l : Filter α} {l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (hl : Filter.HasBasis l p s) (hl' : Filter.HasBasis l' p' s') : Disjoint l l' ↔ ∃ i, p i ∧ ∃ i', p' i' ∧ Disjoint (s i) (s' i')

theorem Disjoint.exists_mem_filter_basis {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l : Filter α} {l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop} {s' : ι' → Set α} (h : Disjoint l l') (hl : Filter.HasBasis l p s) (hl' : Filter.HasBasis l' p' s') : ∃ i, p i ∧ ∃ i', p' i' ∧ Disjoint (s i) (s' i')

theorem Pairwise.exists_mem_filter_basis_of_disjoint {α : Type u_1} {I : Type u_7} [Finite I] {l : I → Filter α} {ι : I → Sort u_6} {p : (i : I) → ι i → Prop} {s : (i : I) → ι i → Set α} (hd : Pairwise (Disjoint on l)) (h : ∀ (i : I), Filter.HasBasis (l i) (p i) (s i)) : ∃ ind, ((i : I) → p i (ind i)) ∧ Pairwise (Disjoint on fun i => s i (ind i))

theorem Set.PairwiseDisjoint.exists_mem_filter_basis {α : Type u_1} {I : Type u_6} {l : I → Filter α} {ι : I → Sort u_7} {p : (i : I) → ι i → Prop} {s : (i : I) → ι i → Set α} {S : Set I} (hd : Set.PairwiseDisjoint S l) (hS : Set.Finite S) (h : ∀ (i : I), Filter.HasBasis (l i) (p i) (s i)) : ∃ ind, ((i : I) → p i (ind i)) ∧ Set.PairwiseDisjoint S fun i => s i (ind i)

theorem Filter.inf_neBot_iff {α : Type u_1} {l : Filter α} {l' : Filter α} : Filter.NeBot (l ⊓ l') ↔ ∀ ⦃s : Set α⦄, s ∈ l → ∀ ⦃s' : Set α⦄, s' ∈ l' → Set.Nonempty (s ∩ s')

theorem Filter.inf_principal_neBot_iff {α : Type u_1} {l : Filter α} {s : Set α} : Filter.NeBot (l ⊓ Filter.principal s) ↔ ∀ (U : Set α), U ∈ l → Set.Nonempty (U ∩ s)

theorem Filter.mem_iff_inf_principal_compl {α : Type u_1} {f : Filter α} {s : Set α} : s ∈ f ↔ f ⊓ Filter.principal sᶜ = ⊥

theorem Filter.not_mem_iff_inf_principal_compl {α : Type u_1} {f : Filter α} {s : Set α} : ¬s ∈ f ↔ Filter.NeBot (f ⊓ Filter.principal sᶜ)

@[simp]

theorem Filter.disjoint_principal_right {α : Type u_1} {f : Filter α} {s : Set α} : Disjoint f (Filter.principal s) ↔ sᶜ ∈ f

@[simp]

theorem Filter.disjoint_principal_left {α : Type u_1} {f : Filter α} {s : Set α} : Disjoint (Filter.principal s) f ↔ sᶜ ∈ f

@[simp]

theorem Filter.disjoint_principal_principal {α : Type u_1} {s : Set α} {t : Set α} : Disjoint (Filter.principal s) (Filter.principal t) ↔ Disjoint s t

theorem Disjoint.filter_principal {α : Type u_1} {s : Set α} {t : Set α} : Disjoint s t → Disjoint (Filter.principal s) (Filter.principal t)

Alias of the reverse direction of Filter.disjoint_principal_principal.

@[simp]

theorem Filter.disjoint_pure_pure {α : Type u_1} {x : α} {y : α} : Disjoint (pure x) (pure y) ↔ x ≠ y

@[simp]

theorem Filter.compl_diagonal_mem_prod {α : Type u_1} {l₁ : Filter α} {l₂ : Filter α} : (Set.diagonal α)ᶜ ∈ l₁ ×ˢ l₂ ↔ Disjoint l₁ l₂

theorem Filter.HasBasis.disjoint_iff_left {α : Type u_1} {ι : Sort u_4} {l : Filter α} {l' : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) : Disjoint l l' ↔ ∃ i, p i ∧ (s i)ᶜ ∈ l'

theorem Filter.HasBasis.disjoint_iff_right {α : Type u_1} {ι : Sort u_4} {l : Filter α} {l' : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) : Disjoint l' l ↔ ∃ i, p i ∧ (s i)ᶜ ∈ l'

theorem Filter.le_iff_forall_inf_principal_compl {α : Type u_1} {f : Filter α} {g : Filter α} : f ≤ g ↔ ∀ (V : Set α), V ∈ g → f ⊓ Filter.principal Vᶜ = ⊥

theorem Filter.inf_neBot_iff_frequently_left {α : Type u_1} {f : Filter α} {g : Filter α} : Filter.NeBot (f ⊓ g) ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → ∃ᶠ (x : α) in g, p x

theorem Filter.inf_neBot_iff_frequently_right {α : Type u_1} {f : Filter α} {g : Filter α} : Filter.NeBot (f ⊓ g) ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in g, p x) → ∃ᶠ (x : α) in f, p x

theorem Filter.HasBasis.eq_biInf {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) : l = ⨅ (i : ι) (x : p i), Filter.principal (s i)

theorem Filter.HasBasis.eq_iInf {α : Type u_1} {ι : Sort u_4} {l : Filter α} {s : ι → Set α} (h : Filter.HasBasis l (fun x => True) s) : l = ⨅ (i : ι), Filter.principal (s i)

theorem Filter.hasBasis_iInf_principal {α : Type u_1} {ι : Sort u_4} {s : ι → Set α} (h : Directed (fun x x_1 => x ≥ x_1) s) [Nonempty ι] : Filter.HasBasis (⨅ (i : ι), Filter.principal (s i)) (fun x => True) s

theorem Filter.hasBasis_iInf_principal_finite {α : Type u_1} {ι : Type u_6} (s : ι → Set α) : Filter.HasBasis (⨅ (i : ι), Filter.principal (s i)) (fun t => Set.Finite t) fun t => ⋂ (i : ι) (_ : 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).

theorem Filter.hasBasis_biInf_principal {α : Type u_1} {β : Type u_2} {s : β → Set α} {S : Set β} (h : DirectedOn (s ⁻¹'o fun x x_1 => x ≥ x_1) S) (ne : Set.Nonempty S) : Filter.HasBasis (⨅ (i : β) (_ : i ∈ S), Filter.principal (s i)) (fun i => i ∈ S) s

theorem Filter.hasBasis_biInf_principal' {α : Type u_1} {ι : Type u_6} {p : ι → Prop} {s : ι → Set α} (h : ∀ (i : ι), p i → ∀ (j : ι), p j → ∃ k, p k ∧ s k ⊆ s i ∧ s k ⊆ s j) (ne : ∃ i, p i) : Filter.HasBasis (⨅ (i : ι) (x : p i), Filter.principal (s i)) p s

theorem Filter.HasBasis.map {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (f : α → β) (hl : Filter.HasBasis l p s) : Filter.HasBasis (Filter.map f l) p fun i => f '' s i

theorem Filter.HasBasis.comap {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (f : β → α) (hl : Filter.HasBasis l p s) : Filter.HasBasis (Filter.comap f l) p fun i => f ⁻¹' s i

theorem Filter.comap_hasBasis {α : Type u_1} {β : Type u_2} (f : α → β) (l : Filter β) : Filter.HasBasis (Filter.comap f l) (fun s => s ∈ l) fun s => f ⁻¹' s

theorem Filter.HasBasis.forall_mem_mem {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) {x : α} : (∀ (t : Set α), t ∈ l → x ∈ t) ↔ ∀ (i : ι), p i → x ∈ s i

theorem Filter.HasBasis.biInf_mem {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} [CompleteLattice β] {f : Set α → β} (h : Filter.HasBasis l p s) (hf : Monotone f) : ⨅ (t : Set α) (_ : t ∈ l), f t = ⨅ (i : ι) (x : p i), f (s i)

theorem Filter.HasBasis.biInter_mem {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {f : Set α → Set β} (h : Filter.HasBasis l p s) (hf : Monotone f) : ⋂ (t : Set α) (_ : t ∈ l), f t = ⋂ (i : ι) (x : p i), f (s i)

theorem Filter.HasBasis.ker {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) : Filter.ker l = ⋂ (i : ι) (x : p i), s i

structure Filter.IsAntitoneBasis {α : Type u_1} {ι'' : Type u_6} [Preorder ι''] (s'' : ι'' → Set α) extends Filter.IsBasis : Prop

• nonempty : ∃ i, True
• inter : ∀ {i j : ι''}, True → True → ∃ k, True ∧ s'' k ⊆ s'' i ∩ s'' j
• antitone : Antitone s''

  The sequence of sets is antitone.

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

structure Filter.HasAntitoneBasis {α : Type u_1} {ι'' : Type u_6} [Preorder ι''] (l : Filter α) (s : ι'' → Set α) extends Filter.HasBasis : Prop

• mem_iff' : ∀ (t : Set α), t ∈ l ↔ ∃ i, True ∧ s✝ i ⊆ t
• antitone : Antitone s✝

  The sequence of sets is antitone.

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.

theorem Filter.HasAntitoneBasis.map {α : Type u_1} {β : Type u_2} {ι'' : Type u_6} [Preorder ι''] {l : Filter α} {s : ι'' → Set α} {m : α → β} (hf : Filter.HasAntitoneBasis l s) : Filter.HasAntitoneBasis (Filter.map m l) fun n => m '' s n

theorem Filter.HasBasis.tendsto_left_iff {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {la : Filter α} {pa : ι → Prop} {sa : ι → Set α} {lb : Filter β} {f : α → β} (hla : Filter.HasBasis la pa sa) : Filter.Tendsto f la lb ↔ ∀ (t : Set β), t ∈ lb → ∃ i, pa i ∧ Set.MapsTo f (sa i) t

theorem Filter.HasBasis.tendsto_right_iff {α : Type u_1} {β : Type u_2} {ι' : Sort u_5} {la : Filter α} {lb : Filter β} {pb : ι' → Prop} {sb : ι' → Set β} {f : α → β} (hlb : Filter.HasBasis lb pb sb) : Filter.Tendsto f la lb ↔ ∀ (i : ι'), pb i → ∀ᶠ (x : α) in la, f x ∈ sb i

theorem Filter.HasBasis.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 : Filter.HasBasis la pa sa) (hlb : Filter.HasBasis lb pb sb) : Filter.Tendsto f la lb ↔ ∀ (ib : ι'), pb ib → ∃ ia, pa ia ∧ ∀ (x : α), x ∈ sa ia → f x ∈ sb ib

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 : Filter.HasBasis la pa sa) (t : Set β) : t ∈ lb → ∃ i, pa i ∧ Set.MapsTo f (sa i) t

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 : Filter.HasBasis lb pb sb) (i : ι') : pb i → ∀ᶠ (x : α) in la, f x ∈ sb i

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 : Filter.HasBasis la pa sa) (hlb : Filter.HasBasis lb pb sb) (ib : ι') : pb ib → ∃ ia, pa ia ∧ Set.MapsTo f (sa ia) (sb ib)

theorem Filter.HasBasis.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 : Filter.HasBasis la pa sa) (hlb : Filter.HasBasis lb pb sb) : Filter.HasBasis (la ×ˢ lb) (fun i => pa i.fst ∧ pb i.snd) fun i => sa i.fst ×ˢ sb i.snd

theorem Filter.HasBasis.prod {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {ι : Type u_6} {ι' : Type u_7} {pa : ι → Prop} {sa : ι → Set α} {pb : ι' → Prop} {sb : ι' → Set β} (hla : Filter.HasBasis la pa sa) (hlb : Filter.HasBasis lb pb sb) : Filter.HasBasis (la ×ˢ lb) (fun i => pa i.fst ∧ pb i.snd) fun i => sa i.fst ×ˢ sb i.snd

theorem Filter.HasBasis.prod_same_index {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {la : Filter α} {sa : ι → Set α} {lb : Filter β} {p : ι → Prop} {sb : ι → Set β} (hla : Filter.HasBasis la p sa) (hlb : Filter.HasBasis lb p sb) (h_dir : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j) : Filter.HasBasis (la ×ˢ lb) p fun i => sa i ×ˢ sb i

theorem Filter.HasBasis.prod_same_index_mono {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {ι : Type u_6} [LinearOrder ι] {p : ι → Prop} {sa : ι → Set α} {sb : ι → Set β} (hla : Filter.HasBasis la p sa) (hlb : Filter.HasBasis lb p sb) (hsa : MonotoneOn sa {i | p i}) (hsb : MonotoneOn sb {i | p i}) : Filter.HasBasis (la ×ˢ lb) p fun i => sa i ×ˢ sb i

theorem Filter.HasBasis.prod_same_index_anti {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {ι : Type u_6} [LinearOrder ι] {p : ι → Prop} {sa : ι → Set α} {sb : ι → Set β} (hla : Filter.HasBasis la p sa) (hlb : Filter.HasBasis lb p sb) (hsa : AntitoneOn sa {i | p i}) (hsb : AntitoneOn sb {i | p i}) : Filter.HasBasis (la ×ˢ lb) p fun i => sa i ×ˢ sb i

theorem Filter.HasBasis.prod_self {α : Type u_1} {ι : Sort u_4} {la : Filter α} {pa : ι → Prop} {sa : ι → Set α} (hl : Filter.HasBasis la pa sa) : Filter.HasBasis (la ×ˢ la) pa fun i => sa i ×ˢ sa i

theorem Filter.mem_prod_self_iff {α : Type u_1} {la : Filter α} {s : Set (α × α)} : s ∈ la ×ˢ la ↔ ∃ t, t ∈ la ∧ t ×ˢ t ⊆ s

theorem Filter.HasAntitoneBasis.prod {α : Type u_1} {β : Type u_2} {ι : Type u_6} [LinearOrder ι] {f : Filter α} {g : Filter β} {s : ι → Set α} {t : ι → Set β} (hf : Filter.HasAntitoneBasis f s) (hg : Filter.HasAntitoneBasis g t) : Filter.HasAntitoneBasis (f ×ˢ g) fun n => s n ×ˢ t n

theorem Filter.HasBasis.coprod {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {ι : Type u_6} {ι' : Type u_7} {pa : ι → Prop} {sa : ι → Set α} {pb : ι' → Prop} {sb : ι' → Set β} (hla : Filter.HasBasis la pa sa) (hlb : Filter.HasBasis lb pb sb) : Filter.HasBasis (Filter.coprod la lb) (fun i => pa i.fst ∧ pb i.snd) fun i => Prod.fst ⁻¹' sa i.fst ∪ Prod.snd ⁻¹' sb i.snd

theorem Filter.map_sigma_mk_comap {α : Type u_1} {β : Type u_2} {π : α → Type u_6} {π' : β → Type u_7} {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)

class Filter.IsCountablyGenerated {α : Type u_1} (f : Filter α) : Prop

• out : ∃ s, Set.Countable s ∧ f = Filter.generate s

  There exists a countable set that generates the filter.

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

structure Filter.IsCountableBasis {α : Type u_1} {ι : Type u_4} (p : ι → Prop) (s : ι → Set α) extends Filter.IsBasis : Prop

• nonempty : ∃ i, p i
• inter : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ s✝ k ⊆ s✝ i ∩ s✝ j
• countable : Set.Countable (setOf p)

  The set of i that satisfy the predicate p is countable.

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

structure Filter.HasCountableBasis {α : Type u_1} {ι : Type u_4} (l : Filter α) (p : ι → Prop) (s : ι → Set α) extends Filter.HasBasis : Prop

• mem_iff' : ∀ (t : Set α), t ∈ l ↔ ∃ i, p i ∧ s✝ i ⊆ t
• countable : Set.Countable (setOf p)

  The set of i that satisfy the predicate p is countable.

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.

structure Filter.CountableFilterBasis (α : Type u_6) extends FilterBasis : Type u_6

• sets : Set (Set α)
• nonempty : Set.Nonempty s.sets
• inter_sets : ∀ {x y : Set α}, x ∈ s.sets → y ∈ s.sets → ∃ z, z ∈ s.sets ∧ z ⊆ x ∩ y
• countable : Set.Countable s.sets

  The set of sets of the filter basis is countable.

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.

instance Filter.Nat.inhabitedCountableFilterBasis : Inhabited (Filter.CountableFilterBasis ℕ)

Equations

• Filter.Nat.inhabitedCountableFilterBasis = { default := { toFilterBasis := default, countable := Filter.Nat.inhabitedCountableFilterBasis.proof_1 } }

theorem Filter.HasCountableBasis.isCountablyGenerated {α : Type u_1} {ι : Type u_4} {f : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasCountableBasis f p s) : Filter.IsCountablyGenerated f

theorem Filter.antitone_seq_of_seq {α : Type u_1} (s : ℕ → Set α) : ∃ t, Antitone t ∧ ⨅ (i : ℕ), Filter.principal (s i) = ⨅ (i : ℕ), Filter.principal (t i)

theorem Filter.countable_biInf_eq_iInf_seq {α : Type u_1} {ι : Type u_4} [CompleteLattice α] {B : Set ι} (Bcbl : Set.Countable B) (Bne : Set.Nonempty B) (f : ι → α) : ∃ x, ⨅ (t : ι) (_ : t ∈ B), f t = ⨅ (i : ℕ), f (x i)

theorem Filter.countable_biInf_eq_iInf_seq' {α : Type u_1} {ι : Type u_4} [CompleteLattice α] {B : Set ι} (Bcbl : Set.Countable B) (f : ι → α) {i₀ : ι} (h : f i₀ = ⊤) : ∃ x, ⨅ (t : ι) (_ : t ∈ B), f t = ⨅ (i : ℕ), f (x i)

theorem Filter.countable_biInf_principal_eq_seq_iInf {α : Type u_1} {B : Set (Set α)} (Bcbl : Set.Countable B) : ∃ x, ⨅ (t : Set α) (_ : t ∈ B), Filter.principal t = ⨅ (i : ℕ), Filter.principal (x i)

theorem Filter.HasAntitoneBasis.mem_iff {α : Type u_1} {ι : Type u_4} [Preorder ι] {l : Filter α} {s : ι → Set α} (hs : Filter.HasAntitoneBasis l s) {t : Set α} : t ∈ l ↔ ∃ i, s i ⊆ t

theorem Filter.HasAntitoneBasis.mem {α : Type u_1} {ι : Type u_4} [Preorder ι] {l : Filter α} {s : ι → Set α} (hs : Filter.HasAntitoneBasis l s) (i : ι) : s i ∈ l

theorem Filter.HasAntitoneBasis.hasBasis_ge {α : Type u_1} {ι : Type u_4} [Preorder ι] [IsDirected ι fun x x_1 => x ≤ x_1] {l : Filter α} {s : ι → Set α} (hs : Filter.HasAntitoneBasis l s) (i : ι) : Filter.HasBasis l (fun j => i ≤ j) s

theorem Filter.HasBasis.exists_antitone_subbasis {α : Type u_1} {ι' : Sort u_5} {f : Filter α} [h : Filter.IsCountablyGenerated f] {p : ι' → Prop} {s : ι' → Set α} (hs : Filter.HasBasis f p s) : ∃ x, ((i : ℕ) → p (x i)) ∧ Filter.HasAntitoneBasis f fun i => s (x i)

If f is countably generated and f.HasBasis 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

theorem Filter.exists_antitone_basis {α : Type u_1} (f : Filter α) [Filter.IsCountablyGenerated f] : ∃ x, Filter.HasAntitoneBasis f x

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

theorem Filter.exists_antitone_seq {α : Type u_1} (f : Filter α) [Filter.IsCountablyGenerated f] : ∃ x, Antitone x ∧ ∀ {s : Set α}, s ∈ f ↔ ∃ i, x i ⊆ s

instance Filter.Inf.isCountablyGenerated {α : Type u_1} (f : Filter α) (g : Filter α) [Filter.IsCountablyGenerated f] [Filter.IsCountablyGenerated g] : Filter.IsCountablyGenerated (f ⊓ g)

Equations

• @Filter.Inf.isCountablyGenerated = @Filter.Inf.isCountablyGenerated.proof_1

instance Filter.map.isCountablyGenerated {α : Type u_1} {β : Type u_2} (l : Filter α) [Filter.IsCountablyGenerated l] (f : α → β) : Filter.IsCountablyGenerated (Filter.map f l)

Equations

• @Filter.map.isCountablyGenerated = @Filter.map.isCountablyGenerated.proof_1

instance Filter.comap.isCountablyGenerated {α : Type u_1} {β : Type u_2} (l : Filter β) [Filter.IsCountablyGenerated l] (f : α → β) : Filter.IsCountablyGenerated (Filter.comap f l)

Equations

• @Filter.comap.isCountablyGenerated = @Filter.comap.isCountablyGenerated.proof_1

instance Filter.Sup.isCountablyGenerated {α : Type u_1} (f : Filter α) (g : Filter α) [Filter.IsCountablyGenerated f] [Filter.IsCountablyGenerated g] : Filter.IsCountablyGenerated (f ⊔ g)

Equations

• @Filter.Sup.isCountablyGenerated = @Filter.Sup.isCountablyGenerated.proof_1

instance Filter.prod.isCountablyGenerated {α : Type u_1} {β : Type u_2} (la : Filter α) (lb : Filter β) [Filter.IsCountablyGenerated la] [Filter.IsCountablyGenerated lb] : Filter.IsCountablyGenerated (la ×ˢ lb)

Equations

• @Filter.prod.isCountablyGenerated = @Filter.prod.isCountablyGenerated.proof_1

instance Filter.coprod.isCountablyGenerated {α : Type u_1} {β : Type u_2} (la : Filter α) (lb : Filter β) [Filter.IsCountablyGenerated la] [Filter.IsCountablyGenerated lb] : Filter.IsCountablyGenerated (Filter.coprod la lb)

Equations

• @Filter.coprod.isCountablyGenerated = @Filter.coprod.isCountablyGenerated.proof_1

theorem Filter.isCountablyGenerated_seq {α : Type u_1} {β : Type u_2} [Countable β] (x : β → Set α) : Filter.IsCountablyGenerated (⨅ (i : β), Filter.principal (x i))

theorem Filter.isCountablyGenerated_of_seq {α : Type u_1} {f : Filter α} (h : ∃ x, f = ⨅ (i : ℕ), Filter.principal (x i)) : Filter.IsCountablyGenerated f

theorem Filter.isCountablyGenerated_biInf_principal {α : Type u_1} {B : Set (Set α)} (h : Set.Countable B) : Filter.IsCountablyGenerated (⨅ (s : Set α) (_ : s ∈ B), Filter.principal s)

theorem Filter.isCountablyGenerated_iff_exists_antitone_basis {α : Type u_1} {f : Filter α} : Filter.IsCountablyGenerated f ↔ ∃ x, Filter.HasAntitoneBasis f x

theorem Filter.isCountablyGenerated_principal {α : Type u_1} (s : Set α) : Filter.IsCountablyGenerated (Filter.principal s)

theorem Filter.isCountablyGenerated_pure {α : Type u_1} (a : α) : Filter.IsCountablyGenerated (pure a)

theorem Filter.isCountablyGenerated_bot {α : Type u_1} : Filter.IsCountablyGenerated ⊥

theorem Filter.isCountablyGenerated_top {α : Type u_1} : Filter.IsCountablyGenerated ⊤

instance Filter.iInf.isCountablyGenerated {ι : Sort u} {α : Type v} [Countable ι] (f : ι → Filter α) [∀ (i : ι), Filter.IsCountablyGenerated (f i)] : Filter.IsCountablyGenerated (⨅ (i : ι), f i)

Equations

• @Filter.iInf.isCountablyGenerated = @Filter.iInf.isCountablyGenerated.proof_1