Documentation

Mathlib.Order.Filter.Bases

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→ Prop, and a map s : ι → set α→ set α, the proposition h : Filter.IsBasis 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.HasBasis l p s (where p : ι → Prop→ Prop and s : ι → set α→ 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)∈ l) that returns some index i such that p i and s i ⊆ t⊆ 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 #

Implementation notes #

As with Set.unionᵢ/bunionᵢ/Set.unionₛ, 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 Filter.HasBasis machinery, e.g., simp only [true_and] or simp only [forall_const] can help with the case p = λ _, true.

structure FilterBasis (α : Type u_1) :
Type u_1
  • Sets of a filter basis.

    sets : Set (Set α)
  • The set of filter basis sets is nonempty.

    nonempty : Set.Nonempty sets
  • The set of filter basis sets is directed downwards.

    inter_sets : ∀ {x y : Set α}, x setsy setsz, z sets z x y

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

    If B is a filter basis on α, and U a subset of α then we can write U ∈ B∈ 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
    def Filter.asBasis {α : Type u_1} (f : Filter α) :

    View a filter as a filter basis.

    Equations
    structure Filter.IsBasis {α : Type u_1} {ι : Sort u_2} (p : ιProp) (s : ιSet α) :
    • There exists at least one i that satisfies p.

      nonempty : i, p i
    • s is directed downwards on i such that p i.

      inter : ∀ {i j : ι}, p ip jk, p k s k s i s j

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

    Instances For
      def Filter.IsBasis.filterBasis {α : Type u_1} {ι : Sort u_2} {p : ιProp} {s : ιSet α} (h : Filter.IsBasis p s) :

      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_2} {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 α) :

      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 α} :
      def Filter.IsBasis.filter {α : Type u_1} {ι : Sort u_2} {p : ιProp} {s : ιSet α} (h : Filter.IsBasis p s) :

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

      Equations
      theorem Filter.IsBasis.mem_filter_iff {α : Type u_1} {ι : Sort u_2} {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_2} {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_2} (l : Filter α) (p : ιProp) (s : ιSet α) :
      • A set t belongs to a filter l iff it includes an element of the basis.

        mem_iff' : ∀ (t : Set α), t l i, p i s i t

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

      Instances For
        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 α)) :

        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.interₛ '' { t | Set.Finite t t s }
        theorem Filter.HasBasis.mem_iff {α : Type u_1} {ι : Sort u_2} {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_2} {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_2} {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_2} {l : Filter α} {p : ιProp} {s : ιSet α} (h : Filter.HasBasis l p s) :
        i, p i
        theorem Filter.HasBasis.nonempty {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ιProp} {s : ιSet α} (h : Filter.HasBasis l p s) :
        theorem Filter.IsBasis.hasBasis {α : Type u_1} {ι : Sort u_2} {p : ιProp} {s : ιSet α} (h : Filter.IsBasis p s) :
        theorem Filter.HasBasis.mem_of_superset {α : Type u_1} {ι : Sort u_2} {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_2} {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_2} {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⊆ t as an element of subtype p.

        Equations
        theorem Filter.HasBasis.property_index {α : Type u_1} {ι : Sort u_2} {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_2} {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_2} {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_2} {l : Filter α} {p : ιProp} {s : ιSet α} (h : Filter.HasBasis l p s) :
        theorem Filter.HasBasis.filter_eq {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ιProp} {s : ιSet α} (h : Filter.HasBasis l p s) :
        theorem Filter.HasBasis.eq_generate {α : Type u_1} {ι : Sort u_2} {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.interₛ '' { t | Set.Finite t t s })
        theorem FilterBasis.hasBasis {α : Type u_1} (B : FilterBasis α) :
        Filter.HasBasis (FilterBasis.filter B) (fun s => s B) id
        theorem Filter.HasBasis.to_has_basis' {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} {l : Filter α} {p : ιProp} {s : ιSet α} {p' : ι'Prop} {s' : ι'Set α} (hl : Filter.HasBasis l p s) (h : ∀ (i : ι), p ii', p' i' s' i' s i) (h' : ∀ (i' : ι'), p' i's' i' l) :
        theorem Filter.HasBasis.to_hasBasis {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} {l : Filter α} {p : ιProp} {s : ιSet α} {p' : ι'Prop} {s' : ι'Set α} (hl : Filter.HasBasis l p s) (h : ∀ (i : ι), p ii', p' i' s' i' s i) (h' : ∀ (i' : ι'), p' i'i, p i s i s' i') :
        theorem Filter.HasBasis.to_subset {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ιProp} {s : ιSet α} (hl : Filter.HasBasis l p s) {t : ιSet α} (h : ∀ (i : ι), p it i s i) (ht : ∀ (i : ι), p it i l) :
        theorem Filter.HasBasis.eventually_iff {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ιProp} {s : ιSet α} (hl : Filter.HasBasis l p s) {q : αProp} :
        Filter.Eventually (fun x => q x) l i, p i (x : α⦄ → x s iq x)
        theorem Filter.HasBasis.frequently_iff {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ιProp} {s : ιSet α} (hl : Filter.HasBasis l p s) {q : αProp} :
        Filter.Frequently (fun x => q x) l ∀ (i : ι), p ix, x s i q x
        theorem Filter.HasBasis.exists_iff {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ιProp} {s : ιSet α} (hl : Filter.HasBasis l p s) {P : Set αProp} (mono : s t : Set α⦄ → s tP tP s) :
        (s, s l P s) i, p i P (s i)
        theorem Filter.HasBasis.forall_iff {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ιProp} {s : ιSet α} (hl : Filter.HasBasis l p s) {P : Set αProp} (mono : s t : Set α⦄ → s tP sP t) :
        ((s : Set α) → s lP s) (i : ι) → p iP (s i)
        theorem Filter.HasBasis.neBot_iff {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ιProp} {s : ιSet α} (hl : Filter.HasBasis l p s) :
        Filter.NeBot l ∀ {i : ι}, p iSet.Nonempty (s i)
        theorem Filter.HasBasis.eq_bot_iff {α : Type u_1} {ι : Sort u_2} {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 sSet.Finite tSet.Nonempty (⋂₀ t)
        theorem Filter.basis_sets {α : Type u_1} (l : Filter α) :
        Filter.HasBasis l (fun s => s l) id
        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 lr, r l P r r t
        theorem Filter.HasBasis.comp_surjective {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} {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_2} {ι' : Sort u_3} {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_2} {l : Filter α} {p : ιProp} {s : ιSet α} (h : Filter.HasBasis l p s) {q : ιProp} (hq : ∀ (i : ι), p ij, 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∧ q j, then {s j | p j ∧ q j}∧ q j} is a basis of l.

        theorem Filter.HasBasis.restrict_subset {α : Type u_1} {ι : Sort u_2} {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∈ l, then {s i | p i ∧ s i ⊆ V}∧ s i ⊆ V}⊆ 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_2} {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_2} {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_2} {ι' : Sort u_3} {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_2} {ι' : Sort u_3} {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 ii', 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_2} {ι' : Sort u_3} {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_3} {l : Filter α} {l' : Filter α} {ι : Type u_1} {ι' : Type u_2} {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_3} {ι : Type u_1} {ι' : ιType u_2} {l : ιFilter α} {p : (i : ι) → ι' iProp} {s : (i : ι) → ι' iSet α} (hl : ∀ (i : ι), Filter.HasBasis (l i) (p i) (s i)) :
        Filter.HasBasis (i, l i) (fun If => Set.Finite If.fst ((i : ι) → i If.fstp i (Prod.snd (Set ι) ((i : ι) → ι' i) If i))) fun If => Set.interᵢ fun i => Set.interᵢ fun h => s i (Prod.snd (Set ι) ((i : ι) → ι' i) If i)
        theorem Filter.hasBasis_infᵢ {α : Type u_3} {ι : Type u_1} {ι' : ιType u_2} {l : ιFilter α} {p : (i : ι) → ι' iProp} {s : (i : ι) → ι' iSet α} (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 => Set.interᵢ fun i => s (i) (Sigma.snd (Set ι) (fun I => (i : I) → ι' i) If i)
        theorem Filter.hasBasis_infᵢ_of_directed' {α : Type u_3} {ι : Type u_1} {ι' : ιType u_2} [inst : Nonempty ι] {l : ιFilter α} (s : (i : ι) → ι' iSet α) (p : (i : ι) → ι' iProp) (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_infᵢ_of_directed {α : Type u_3} {ι : Type u_1} {ι' : Type u_2} [inst : 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_binfᵢ_of_directed' {α : Type u_3} {ι : Type u_1} {ι' : ιType u_2} {dom : Set ι} (hdom : Set.Nonempty dom) {l : ιFilter α} (s : (i : ι) → ι' iSet α) (p : (i : ι) → ι' iProp) (hl : ∀ (i : ι), i domFilter.HasBasis (l i) (p i) (s i)) (h : DirectedOn (l ⁻¹'o GE.ge) dom) :
        Filter.HasBasis (i, h, l i) (fun ii' => ii'.fst dom p ii'.fst ii'.snd) fun ii' => s ii'.fst ii'.snd
        theorem Filter.hasBasis_binfᵢ_of_directed {α : Type u_3} {ι : Type u_1} {ι' : Type u_2} {dom : Set ι} (hdom : Set.Nonempty dom) {l : ιFilter α} (s : ιι'Set α) (p : ιι'Prop) (hl : ∀ (i : ι), i domFilter.HasBasis (l i) (p i) (s i)) (h : DirectedOn (l ⁻¹'o GE.ge) dom) :
        Filter.HasBasis (i, h, 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_2} {ι' : Sort u_3} {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_3} {l : Filter α} {l' : Filter α} {ι : Type u_1} {ι' : Type u_2} {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_3} {ι : Sort u_1} {ι' : ιType u_2} {l : ιFilter α} {p : (i : ι) → ι' iProp} {s : (i : ι) → ι' iSet α} (hl : ∀ (i : ι), Filter.HasBasis (l i) (p i) (s i)) :
        Filter.HasBasis (i, l i) (fun f => (i : ι) → p i (f i)) fun f => Set.unionᵢ fun i => s i (f i)
        theorem Filter.HasBasis.sup_principal {α : Type u_1} {ι : Sort u_2} {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_2} {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_2} {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_2} {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_2} {ι' : Sort u_3} {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_2} {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_2} {l : Filter α} {p : ιProp} {s : ιSet α} (hl : Filter.HasBasis l p s) {t : Set α} :
        Filter.NeBot (l Filter.principal t) ∀ ⦃i : ι⦄, p iSet.Nonempty (s i t)
        theorem Filter.HasBasis.disjoint_iff {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} {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_2} {ι' : Sort u_3} {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_2} {I : Type u_1} [inst : Finite I] {l : IFilter α} {ι : ISort u_3} {p : (i : I) → ι iProp} {s : (i : I) → ι iSet α} (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_2} {I : Type u_1} {l : IFilter α} {ι : ISort u_3} {p : (i : I) → ι iProp} {s : (i : I) → ι iSet α} {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 lSet.Nonempty (U s)
        @[simp]
        theorem Filter.disjoint_principal_right {α : Type u_1} {f : Filter α} {s : Set α} :
        @[simp]
        theorem Filter.disjoint_principal_left {α : Type u_1} {f : Filter α} {s : Set α} :
        theorem Disjoint.filter_principal {α : Type u_1} {s : Set α} {t : Set α} :

        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 α Filter.prod l₁ l₂ Disjoint l₁ l₂
        theorem Filter.HasBasis.disjoint_iff_left {α : Type u_1} {ι : Sort u_2} {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_2} {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 gf Filter.principal (V) =
        theorem Filter.inf_neBot_iff_frequently_left {α : Type u_1} {f : Filter α} {g : Filter α} :
        Filter.NeBot (f g) ∀ {p : αProp}, Filter.Eventually (fun x => p x) fFilter.Frequently (fun x => p x) g
        theorem Filter.inf_neBot_iff_frequently_right {α : Type u_1} {f : Filter α} {g : Filter α} :
        Filter.NeBot (f g) ∀ {p : αProp}, Filter.Eventually (fun x => p x) gFilter.Frequently (fun x => p x) f
        theorem Filter.HasBasis.eq_binfᵢ {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ιProp} {s : ιSet α} (h : Filter.HasBasis l p s) :
        l = i, _hi, Filter.principal (s i)
        theorem Filter.HasBasis.eq_infᵢ {α : Type u_1} {ι : Sort u_2} {l : Filter α} {s : ιSet α} (h : Filter.HasBasis l (fun x => True) s) :
        l = i, Filter.principal (s i)
        theorem Filter.hasBasis_infᵢ_principal {α : Type u_1} {ι : Sort u_2} {s : ιSet α} (h : Directed (fun x x_1 => x x_1) s) [inst : Nonempty ι] :
        Filter.HasBasis (i, Filter.principal (s i)) (fun x => True) s
        theorem Filter.hasBasis_infᵢ_principal_finite {α : Type u_2} {ι : Type u_1} (s : ιSet α) :
        Filter.HasBasis (i, Filter.principal (s i)) (fun t => Set.Finite t) fun t => Set.interᵢ fun i => Set.interᵢ fun h => s i

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

        theorem Filter.hasBasis_binfᵢ_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, h, Filter.principal (s i)) (fun i => i S) s
        theorem Filter.hasBasis_binfᵢ_principal' {α : Type u_2} {ι : Type u_1} {p : ιProp} {s : ιSet α} (h : ∀ (i : ι), p i∀ (j : ι), p jk, p k s k s i s k s j) (ne : i, p i) :
        Filter.HasBasis (i, _h, Filter.principal (s i)) p s
        theorem Filter.HasBasis.map {α : Type u_1} {β : Type u_3} {ι : Sort u_2} {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_3} {ι : Sort u_2} {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_2} {β : Type u_1} (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_2} {l : Filter α} {p : ιProp} {s : ιSet α} (h : Filter.HasBasis l p s) {x : α} :
        (∀ (t : Set α), t lx t) ∀ (i : ι), p ix s i
        theorem Filter.HasBasis.binfᵢ_mem {α : Type u_2} {β : Type u_1} {ι : Sort u_3} {l : Filter α} {p : ιProp} {s : ιSet α} [inst : CompleteLattice β] {f : Set αβ} (h : Filter.HasBasis l p s) (hf : Monotone f) :
        (t, h, f t) = i, _hi, f (s i)
        theorem Filter.HasBasis.binterᵢ_mem {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {l : Filter α} {p : ιProp} {s : ιSet α} {f : Set αSet β} (h : Filter.HasBasis l p s) (hf : Monotone f) :
        (Set.interᵢ fun t => Set.interᵢ fun h => f t) = Set.interᵢ fun i => Set.interᵢ fun _hi => f (s i)
        theorem Filter.HasBasis.interₛ_sets {α : Type u_1} {ι : Sort u_2} {l : Filter α} {p : ιProp} {s : ιSet α} (h : Filter.HasBasis l p s) :
        ⋂₀ l.sets = Set.interᵢ fun i => Set.interᵢ fun _hi => s i
        structure Filter.IsAntitoneBasis {α : Type u_1} {ι'' : Type u_2} [inst : Preorder ι''] (s'' : ι''Set α) extends Filter.IsBasis :
        • The sequence of sets is antitone.

          antitone : Antitone s''

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

        Instances For
          structure Filter.HasAntitoneBasis {α : Type u_1} {ι'' : Type u_2} [inst : Preorder ι''] (l : Filter α) (s : ι''Set α) extends Filter.HasBasis :
          • The sequence of sets is antitone.

            antitone : Antitone s

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

          Instances For
            theorem Filter.HasAntitoneBasis.map {α : Type u_1} {β : Type u_3} {ι'' : Type u_2} [inst : Preorder ι''] {l : Filter α} {s : ι''Set α} {m : αβ} (hf : Filter.HasAntitoneBasis l s) :
            theorem Filter.HasBasis.tendsto_left_iff {α : Type u_1} {β : Type u_3} {ι : Sort u_2} {la : Filter α} {pa : ιProp} {sa : ιSet α} {lb : Filter β} {f : αβ} (hla : Filter.HasBasis la pa sa) :
            Filter.Tendsto f la lb ∀ (t : Set β), t lbi, pa i Set.MapsTo f (sa i) t
            theorem Filter.HasBasis.tendsto_right_iff {α : Type u_3} {β : Type u_1} {ι' : Sort u_2} {la : Filter α} {lb : Filter β} {pb : ι'Prop} {sb : ι'Set β} {f : αβ} (hlb : Filter.HasBasis lb pb sb) :
            Filter.Tendsto f la lb ∀ (i : ι'), pb iFilter.Eventually (fun x => f x sb i) la
            theorem Filter.HasBasis.tendsto_iff {α : Type u_1} {β : Type u_3} {ι : Sort u_2} {ι' : Sort u_4} {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 ibia, pa ia ∀ (x : α), x sa iaf x sb ib
            theorem Filter.Tendsto.basis_left {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {la : Filter α} {pa : ιProp} {sa : ιSet α} {lb : Filter β} {f : αβ} (H : Filter.Tendsto f la lb) (hla : Filter.HasBasis la pa sa) (t : Set β) :
            t lbi, pa i Set.MapsTo f (sa i) t
            theorem Filter.Tendsto.basis_right {α : Type u_1} {β : Type u_2} {ι' : Sort u_3} {la : Filter α} {lb : Filter β} {pb : ι'Prop} {sb : ι'Set β} {f : αβ} (H : Filter.Tendsto f la lb) (hlb : Filter.HasBasis lb pb sb) (i : ι') :
            pb iFilter.Eventually (fun x => f x sb i) la
            theorem Filter.Tendsto.basis_both {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {ι' : Sort u_4} {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 ibia, pa ia Set.MapsTo f (sa ia) (sb ib)
            theorem Filter.HasBasis.prod_pprod {α : Type u_1} {β : Type u_3} {ι : Sort u_2} {ι' : Sort u_4} {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 (Filter.prod la lb) (fun i => pa i.fst pb i.snd) fun i => sa i.fst ×ˢ sb i.snd
            theorem Filter.HasBasis.prod {α : Type u_3} {β : Type u_4} {la : Filter α} {lb : Filter β} {ι : Type u_1} {ι' : Type u_2} {pa : ιProp} {sa : ιSet α} {pb : ι'Prop} {sb : ι'Set β} (hla : Filter.HasBasis la pa sa) (hlb : Filter.HasBasis lb pb sb) :
            Filter.HasBasis (Filter.prod 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_2} {β : Type u_1} {ι : Sort u_3} {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 ip jk, p k sa k sa i sb k sb j) :
            Filter.HasBasis (Filter.prod la lb) p fun i => sa i ×ˢ sb i
            theorem Filter.HasBasis.prod_same_index_mono {α : Type u_2} {β : Type u_3} {la : Filter α} {lb : Filter β} {ι : Type u_1} [inst : 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 (Filter.prod la lb) p fun i => sa i ×ˢ sb i
            theorem Filter.HasBasis.prod_same_index_anti {α : Type u_2} {β : Type u_3} {la : Filter α} {lb : Filter β} {ι : Type u_1} [inst : 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 (Filter.prod la lb) p fun i => sa i ×ˢ sb i
            theorem Filter.HasBasis.prod_self {α : Type u_1} {ι : Sort u_2} {la : Filter α} {pa : ιProp} {sa : ιSet α} (hl : Filter.HasBasis la pa sa) :
            Filter.HasBasis (Filter.prod la la) pa fun i => sa i ×ˢ sa i
            theorem Filter.mem_prod_self_iff {α : Type u_1} {la : Filter α} {s : Set (α × α)} :
            s Filter.prod la la t, t la t ×ˢ t s
            theorem Filter.HasAntitoneBasis.prod {α : Type u_2} {β : Type u_3} {ι : Type u_1} [inst : LinearOrder ι] {f : Filter α} {g : Filter β} {s : ιSet α} {t : ιSet β} (hf : Filter.HasAntitoneBasis f s) (hg : Filter.HasAntitoneBasis g t) :
            theorem Filter.HasBasis.coprod {α : Type u_3} {β : Type u_4} {la : Filter α} {lb : Filter β} {ι : Type u_1} {ι' : Type u_2} {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_3} {β : Type u_4} {π : αType u_1} {π' : βType u_2} {f : αβ} (hf : Function.Injective f) (g : (a : α) → π aπ' (f a)) (a : α) (l : Filter (π' (f a))) :
            class Filter.IsCountablyGenerated {α : Type u_1} (f : Filter α) :

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

            Instances
              structure Filter.IsCountableBasis {α : Type u_1} {ι : Type u_2} (p : ιProp) (s : ιSet α) extends Filter.IsBasis :
              • The set of i that satisfy the predicate p is countable.

                countable : Set.Countable (setOf p)

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

              Instances For
                structure Filter.HasCountableBasis {α : Type u_1} {ι : Type u_2} (l : Filter α) (p : ιProp) (s : ιSet α) extends Filter.HasBasis :
                • The set of i that satisfy the predicate p is countable.

                  countable : Set.Countable (setOf p)

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

                Instances For
                  structure Filter.CountableFilterBasis (α : Type u_1) extends FilterBasis :
                  Type u_1
                  • The set of sets of the filter basis is countable.

                    countable : Set.Countable toFilterBasis.sets

                  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
                    theorem Filter.HasCountableBasis.isCountablyGenerated {α : Type u_1} {ι : Type u_2} {f : Filter α} {p : ιProp} {s : ιSet α} (h : Filter.HasCountableBasis f p s) :
                    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_binfᵢ_eq_infᵢ_seq {α : Type u_1} {ι : Type u_2} [inst : CompleteLattice α] {B : Set ι} (Bcbl : Set.Countable B) (Bne : Set.Nonempty B) (f : ια) :
                    x, (t, h, f t) = i, f (x i)
                    theorem Filter.countable_binfᵢ_eq_infᵢ_seq' {α : Type u_1} {ι : Type u_2} [inst : CompleteLattice α] {B : Set ι} (Bcbl : Set.Countable B) (f : ια) {i₀ : ι} (h : f i₀ = ) :
                    x, (t, h, f t) = i, f (x i)
                    theorem Filter.countable_binfᵢ_principal_eq_seq_infᵢ {α : Type u_1} {B : Set (Set α)} (Bcbl : Set.Countable B) :
                    x, (t, h, Filter.principal t) = i, Filter.principal (x i)
                    theorem Filter.HasAntitoneBasis.mem_iff {α : Type u_2} {ι : Type u_1} [inst : Preorder ι] {l : Filter α} {s : ιSet α} (hs : Filter.HasAntitoneBasis l s) {t : Set α} :
                    t l i, s i t
                    theorem Filter.HasAntitoneBasis.mem {α : Type u_2} {ι : Type u_1} [inst : Preorder ι] {l : Filter α} {s : ιSet α} (hs : Filter.HasAntitoneBasis l s) (i : ι) :
                    s i l
                    theorem Filter.HasAntitoneBasis.hasBasis_ge {α : Type u_2} {ι : Type u_1} [inst : Preorder ι] [inst : 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_2} {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

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

                    theorem Filter.exists_antitone_seq {α : Type u_1} (f : Filter α) [inst : Filter.IsCountablyGenerated f] :
                    x, Antitone x ∀ {s : Set α}, s f i, x i s
                    theorem Filter.isCountablyGenerated_seq {α : Type u_2} {β : Type u_1} [inst : Countable β] (x : βSet α) :