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, 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 #

Implementation notes #

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

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_iff] or simp only [forall_const] can help with the case p = fun _ ↦ True.

structure FilterBasis (α : 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.

  • sets : Set (Set α)

    Sets of a filter basis.

  • nonempty : self.sets.Nonempty

    The set of filter basis sets is nonempty.

  • inter_sets : ∀ {x y : Set α}, x self.setsy self.setszself.sets, z x y

    The set of filter basis sets is directed downwards.

Instances For
    theorem FilterBasis.nonempty {α : Type u_6} (self : FilterBasis α) :
    self.sets.Nonempty

    The set of filter basis sets is nonempty.

    theorem FilterBasis.inter_sets {α : Type u_6} (self : FilterBasis α) {x : Set α} {y : Set α} :
    x self.setsy self.setszself.sets, z x y

    The set of filter basis sets is directed downwards.

    instance FilterBasis.nonempty_sets {α : Type u_1} (B : FilterBasis α) :
    Nonempty B.sets
    Equations
    • =

    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 (B : FilterBasis α) (U : Set α) => 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
    • f.asBasis = { sets := f.sets, nonempty := , inter_sets := }
    Instances For
      structure Filter.IsBasis {α : Type u_1} {ι : Sort u_4} (p : ιProp) (s : ιSet α) :

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

      • nonempty : ∃ (i : ι), p i

        There exists at least one i that satisfies p.

      • inter : ∀ {i j : ι}, p ip j∃ (k : ι), p k s k s i s j

        s is directed downwards on i such that p i.

      Instances For
        theorem Filter.IsBasis.nonempty {α : Type u_1} {ι : Sort u_4} {p : ιProp} {s : ιSet α} (self : Filter.IsBasis p s) :
        ∃ (i : ι), p i

        There exists at least one i that satisfies p.

        theorem Filter.IsBasis.inter {α : Type u_1} {ι : Sort u_4} {p : ιProp} {s : ιSet α} (self : Filter.IsBasis p s) {i : ι} {j : ι} :
        p ip j∃ (k : ι), p k s k s i s j

        s is directed downwards on i such that p i.

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

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

        Equations
        • h.filterBasis = { sets := {t : Set α | ∃ (i : ι), p i s i = t}, nonempty := , inter_sets := }
        Instances For
          theorem Filter.IsBasis.mem_filterBasis_iff {α : Type u_1} {ι : Sort u_4} {p : ιProp} {s : ιSet α} (h : Filter.IsBasis p s) {U : Set α} :
          U h.filterBasis ∃ (i : ι), p i s i = U
          def FilterBasis.filter {α : Type u_1} (B : FilterBasis α) :

          The filter associated to a filter basis.

          Equations
          • B.filter = { sets := {s : Set α | tB, t s}, univ_sets := , sets_of_superset := , inter_sets := }
          Instances For
            theorem FilterBasis.mem_filter_iff {α : Type u_1} (B : FilterBasis α) {U : Set α} :
            U B.filter sB, s U
            theorem FilterBasis.mem_filter_of_mem {α : Type u_1} (B : FilterBasis α) {U : Set α} :
            U BU B.filter
            theorem FilterBasis.eq_iInf_principal {α : Type u_1} (B : FilterBasis α) :
            B.filter = ⨅ (s : B.sets), Filter.principal s
            theorem FilterBasis.generate {α : Type u_1} (B : FilterBasis α) :
            Filter.generate B.sets = B.filter
            def Filter.IsBasis.filter {α : Type u_1} {ι : Sort u_4} {p : ιProp} {s : ιSet α} (h : Filter.IsBasis p s) :

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

            Equations
            • h.filter = h.filterBasis.filter
            Instances For
              theorem Filter.IsBasis.mem_filter_iff {α : Type u_1} {ι : Sort u_4} {p : ιProp} {s : ιSet α} (h : Filter.IsBasis p s) {U : Set α} :
              U h.filter ∃ (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) :
              h.filter = Filter.generate {U : Set α | ∃ (i : ι), p i s i = U}
              structure Filter.HasBasis {α : Type u_1} {ι : Sort u_4} (l : Filter α) (p : ιProp) (s : ιSet α) :

              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.

              • 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.

              Instances For
                theorem Filter.HasBasis.mem_iff' {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} (self : l.HasBasis p s) (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.

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

                The smallest filter basis containing a given collection of sets.

                Equations
                Instances For
                  theorem Filter.FilterBasis.ofSets_sets {α : Type u_1} (s : Set (Set α)) :
                  (Filter.FilterBasis.ofSets s).sets = Set.sInter '' {t : Set (Set α) | t.Finite t s}
                  theorem Filter.HasBasis.mem_iff {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} {t : Set α} (hl : l.HasBasis 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 : l.HasBasis p s) (hl' : l'.HasBasis p s) :
                  l = l'
                  theorem Filter.hasBasis_iff {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} :
                  l.HasBasis 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 : l.HasBasis p s) :
                  ∃ (i : ι), p i
                  theorem Filter.HasBasis.nonempty {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} (h : l.HasBasis p s) :
                  theorem Filter.IsBasis.hasBasis {α : Type u_1} {ι : Sort u_4} {p : ιProp} {s : ιSet α} (h : Filter.IsBasis p s) :
                  h.filter.HasBasis p s
                  theorem Filter.HasBasis.mem_of_superset {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} {t : Set α} {i : ι} (hl : l.HasBasis 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 : l.HasBasis 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 : l.HasBasis 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
                  • h.index t ht = .choose,
                  Instances For
                    theorem Filter.HasBasis.property_index {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} {t : Set α} (h : l.HasBasis p s) (ht : t l) :
                    p (h.index t ht)
                    theorem Filter.HasBasis.set_index_mem {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} {t : Set α} (h : l.HasBasis p s) (ht : t l) :
                    s (h.index t ht) l
                    theorem Filter.HasBasis.set_index_subset {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} {t : Set α} (h : l.HasBasis p s) (ht : t l) :
                    s (h.index t ht) t
                    theorem Filter.HasBasis.isBasis {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} (h : l.HasBasis p s) :
                    theorem Filter.HasBasis.filter_eq {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} (h : l.HasBasis p s) :
                    .filter = l
                    theorem Filter.HasBasis.eq_generate {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} (h : l.HasBasis p s) :
                    l = Filter.generate {U : Set α | ∃ (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 (Set α) | t.Finite t s})
                    theorem FilterBasis.hasBasis {α : Type u_1} (B : FilterBasis α) :
                    B.filter.HasBasis (fun (s : Set α) => 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 : l.HasBasis p s) (h : ∀ (i : ι), p i∃ (i' : ι'), p' i' s' i' s i) (h' : ∀ (i' : ι'), p' i's' i' l) :
                    l.HasBasis 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 : l.HasBasis 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.HasBasis p' s'
                    theorem Filter.HasBasis.congr {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} (hl : l.HasBasis p s) {p' : ιProp} {s' : ιSet α} (hp : ∀ (i : ι), p i p' i) (hs : ∀ (i : ι), p is i = s' i) :
                    l.HasBasis p' s'
                    theorem Filter.HasBasis.to_subset {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} (hl : l.HasBasis p s) {t : ιSet α} (h : ∀ (i : ι), p it i s i) (ht : ∀ (i : ι), p it i l) :
                    l.HasBasis p t
                    theorem Filter.HasBasis.eventually_iff {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} (hl : l.HasBasis p s) {q : αProp} :
                    (∀ᶠ (x : α) in l, q x) ∃ (i : ι), p i ∀ ⦃x : α⦄, x s iq x
                    theorem Filter.HasBasis.frequently_iff {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} (hl : l.HasBasis p s) {q : αProp} :
                    (∃ᶠ (x : α) in l, q x) ∀ (i : ι), p ixs i, q x
                    theorem Filter.HasBasis.exists_iff {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} (hl : l.HasBasis p s) {P : Set αProp} (mono : ∀ ⦃s t : Set α⦄, s tP tP s) :
                    (∃ sl, 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 : l.HasBasis p s) {P : Set αProp} (mono : ∀ ⦃s t : Set α⦄, s tP sP t) :
                    (∀ sl, P s) ∀ (i : ι), p iP (s i)
                    theorem Filter.HasBasis.neBot_iff {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} (hl : l.HasBasis p s) :
                    l.NeBot ∀ {i : ι}, p i(s i).Nonempty
                    theorem Filter.HasBasis.eq_bot_iff {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} (hl : l.HasBasis p s) :
                    l = ∃ (i : ι), p i s i =
                    theorem Filter.generate_neBot_iff {α : Type u_1} {s : Set (Set α)} :
                    (Filter.generate s).NeBot ts, t.Finite(⋂₀ t).Nonempty
                    theorem Filter.basis_sets {α : Type u_1} (l : Filter α) :
                    l.HasBasis (fun (s : Set α) => s l) id
                    theorem Filter.asBasis_filter {α : Type u_1} (f : Filter α) :
                    f.asBasis.filter = f
                    theorem Filter.hasBasis_self {α : Type u_1} {l : Filter α} {P : Set αProp} :
                    l.HasBasis (fun (s : Set α) => s l P s) id tl, rl, 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 : l.HasBasis p s) {g : ι'ι} (hg : Function.Surjective g) :
                    l.HasBasis (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 : l.HasBasis p s) (e : ι' ι) :
                    l.HasBasis (p e) (s e)
                    theorem Filter.HasBasis.to_image_id' {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} (h : l.HasBasis p s) :
                    l.HasBasis (fun (t : Set α) => ∃ (i : ι), p i s i = t) id
                    theorem Filter.HasBasis.to_image_id {α : Type u_1} {l : Filter α} {ι : Type u_6} {p : ιProp} {s : ιSet α} (h : l.HasBasis p s) :
                    l.HasBasis (fun (x : Set α) => x s '' {i : ι | p i}) id
                    theorem Filter.HasBasis.restrict {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} (h : l.HasBasis p s) {q : ιProp} (hq : ∀ (i : ι), p i∃ (j : ι), p j q j s j s i) :
                    l.HasBasis (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 : l.HasBasis p s) {V : Set α} (hV : V l) :
                    l.HasBasis (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 : l.HasBasis (fun (s : Set α) => s l p s) id) {V : Set α} (hV : V l) :
                    l.HasBasis (fun (s : Set α) => 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' : l'.HasBasis 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 : l.HasBasis p s) :
                    l l' tl', ∃ (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 : l.HasBasis p s) (hl' : l'.HasBasis 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 : l.HasBasis p s) (hl' : l'.HasBasis 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 : l.HasBasis p s) (hl' : l'.HasBasis p' s') :
                    (l l').HasBasis (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 : l.HasBasis p s) (hl' : l'.HasBasis p' s') :
                    (l l').HasBasis (fun (i : ι × ι') => p i.1 p' i.2) fun (i : ι × ι') => s i.1 s' i.2
                    theorem Filter.hasBasis_iInf' {α : Type u_1} {ι : Type u_6} {ι' : ιType u_7} {l : ιFilter α} {p : (i : ι) → ι' iProp} {s : (i : ι) → ι' iSet α} (hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)) :
                    (⨅ (i : ι), l i).HasBasis (fun (If : Set ι × ((i : ι) → ι' i)) => If.1.Finite iIf.1, p i (If.2 i)) fun (If : Set ι × ((i : ι) → ι' i)) => iIf.1, s i (If.2 i)
                    theorem Filter.hasBasis_iInf {α : Type u_1} {ι : Type u_6} {ι' : ιType u_7} {l : ιFilter α} {p : (i : ι) → ι' iProp} {s : (i : ι) → ι' iSet α} (hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)) :
                    (⨅ (i : ι), l i).HasBasis (fun (If : (I : Set ι) × ((i : I) → ι' i)) => If.fst.Finite ∀ (i : If.fst), p (↑i) (If.snd i)) fun (If : (I : Set ι) × ((i : I) → ι' i)) => ⋂ (i : If.fst), s (↑i) (If.snd i)
                    theorem Filter.hasBasis_iInf_of_directed' {α : Type u_1} {ι : Type u_6} {ι' : ιType u_7} [Nonempty ι] {l : ιFilter α} (s : (i : ι) → ι' iSet α) (p : (i : ι) → ι' iProp) (hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)) (h : Directed (fun (x1 x2 : Filter α) => x1 x2) l) :
                    (⨅ (i : ι), l i).HasBasis (fun (ii' : (i : ι) × ι' i) => p ii'.fst ii'.snd) fun (ii' : (i : ι) × ι' i) => 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 : ι), (l i).HasBasis (p i) (s i)) (h : Directed (fun (x1 x2 : Filter α) => x1 x2) l) :
                    (⨅ (i : ι), l i).HasBasis (fun (ii' : ι × ι') => p ii'.1 ii'.2) fun (ii' : ι × ι') => s ii'.1 ii'.2
                    theorem Filter.hasBasis_biInf_of_directed' {α : Type u_1} {ι : Type u_6} {ι' : ιType u_7} {dom : Set ι} (hdom : dom.Nonempty) {l : ιFilter α} (s : (i : ι) → ι' iSet α) (p : (i : ι) → ι' iProp) (hl : idom, (l i).HasBasis (p i) (s i)) (h : DirectedOn (l ⁻¹'o GE.ge) dom) :
                    (⨅ idom, l i).HasBasis (fun (ii' : (i : ι) × ι' i) => ii'.fst dom p ii'.fst ii'.snd) fun (ii' : (i : ι) × ι' i) => s ii'.fst ii'.snd
                    theorem Filter.hasBasis_biInf_of_directed {α : Type u_1} {ι : Type u_6} {ι' : Type u_7} {dom : Set ι} (hdom : dom.Nonempty) {l : ιFilter α} (s : ιι'Set α) (p : ιι'Prop) (hl : idom, (l i).HasBasis (p i) (s i)) (h : DirectedOn (l ⁻¹'o GE.ge) dom) :
                    (⨅ idom, l i).HasBasis (fun (ii' : ι × ι') => ii'.1 dom p ii'.1 ii'.2) fun (ii' : ι × ι') => s ii'.1 ii'.2
                    theorem Filter.hasBasis_principal {α : Type u_1} (t : Set α) :
                    (Filter.principal t).HasBasis (fun (x : Unit) => True) fun (x : Unit) => t
                    theorem Filter.hasBasis_pure {α : Type u_1} (x : α) :
                    (pure x).HasBasis (fun (x : Unit) => True) fun (x_1 : Unit) => {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 : l.HasBasis p s) (hl' : l'.HasBasis p' s') :
                    (l l').HasBasis (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 : l.HasBasis p s) (hl' : l'.HasBasis p' s') :
                    (l l').HasBasis (fun (i : ι × ι') => p i.1 p' i.2) fun (i : ι × ι') => s i.1 s' i.2
                    theorem Filter.hasBasis_iSup {α : Type u_1} {ι : Sort u_6} {ι' : ιType u_7} {l : ιFilter α} {p : (i : ι) → ι' iProp} {s : (i : ι) → ι' iSet α} (hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)) :
                    (⨆ (i : ι), l i).HasBasis (fun (f : (i : ι) → ι' i) => ∀ (i : ι), p i (f i)) fun (f : (i : ι) → ι' i) => ⋃ (i : ι), s i (f i)
                    theorem Filter.HasBasis.sup_principal {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} (hl : l.HasBasis p s) (t : Set α) :
                    (l Filter.principal t).HasBasis p fun (i : ι) => s i t
                    theorem Filter.HasBasis.sup_pure {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} (hl : l.HasBasis p s) (x : α) :
                    (l pure x).HasBasis p fun (i : ι) => s i {x}
                    theorem Filter.HasBasis.inf_principal {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} (hl : l.HasBasis p s) (s' : Set α) :
                    (l Filter.principal s').HasBasis p fun (i : ι) => s i s'
                    theorem Filter.HasBasis.principal_inf {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} (hl : l.HasBasis p s) (s' : Set α) :
                    (Filter.principal s' l).HasBasis 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 : l.HasBasis p s) (hl' : l'.HasBasis p' s') :
                    (l l').NeBot ∀ ⦃i : ι⦄, p i∀ ⦃i' : ι'⦄, p' i'(s i s' i').Nonempty
                    theorem Filter.HasBasis.inf_neBot_iff {α : Type u_1} {ι : Sort u_4} {l : Filter α} {l' : Filter α} {p : ιProp} {s : ιSet α} (hl : l.HasBasis p s) :
                    (l l').NeBot ∀ ⦃i : ι⦄, p i∀ ⦃s' : Set α⦄, s' l'(s i s').Nonempty
                    theorem Filter.HasBasis.inf_principal_neBot_iff {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} (hl : l.HasBasis p s) {t : Set α} :
                    (l Filter.principal t).NeBot ∀ ⦃i : ι⦄, p i(s i t).Nonempty
                    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 : l.HasBasis p s) (hl' : l'.HasBasis 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 : l.HasBasis p s) (hl' : l'.HasBasis 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 : IFilter α} {ι : ISort u_6} {p : (i : I) → ι iProp} {s : (i : I) → ι iSet α} (hd : Pairwise (Disjoint on l)) (h : ∀ (i : I), (l i).HasBasis (p i) (s i)) :
                    ∃ (ind : (i : I) → ι i), (∀ (i : I), p i (ind i)) Pairwise (Disjoint on fun (i : I) => s i (ind i))
                    theorem Set.PairwiseDisjoint.exists_mem_filter_basis {α : Type u_1} {I : Type u_6} {l : IFilter α} {ι : ISort u_7} {p : (i : I) → ι iProp} {s : (i : I) → ι iSet α} {S : Set I} (hd : S.PairwiseDisjoint l) (hS : S.Finite) (h : ∀ (i : I), (l i).HasBasis (p i) (s i)) :
                    ∃ (ind : (i : I) → ι i), (∀ (i : I), p i (ind i)) S.PairwiseDisjoint fun (i : I) => s i (ind i)
                    theorem Filter.inf_neBot_iff {α : Type u_1} {l : Filter α} {l' : Filter α} :
                    (l l').NeBot ∀ ⦃s : Set α⦄, s l∀ ⦃s' : Set α⦄, s' l'(s s').Nonempty
                    theorem Filter.inf_principal_neBot_iff {α : Type u_1} {l : Filter α} {s : Set α} :
                    (l Filter.principal s).NeBot Ul, (U s).Nonempty
                    theorem Filter.not_mem_iff_inf_principal_compl {α : Type u_1} {f : Filter α} {s : Set α} :
                    sf (f Filter.principal s).NeBot
                    @[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 α) 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 : l.HasBasis 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 : l.HasBasis 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 Vg, f Filter.principal V =
                    theorem Filter.inf_neBot_iff_frequently_left {α : Type u_1} {f : Filter α} {g : Filter α} :
                    (f g).NeBot ∀ {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 α} :
                    (f g).NeBot ∀ {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 : l.HasBasis p s) :
                    l = ⨅ (i : ι), ⨅ (_ : p i), Filter.principal (s i)
                    theorem Filter.HasBasis.eq_iInf {α : Type u_1} {ι : Sort u_4} {l : Filter α} {s : ιSet α} (h : l.HasBasis (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 (x1 x2 : Set α) => x1 x2) s) [Nonempty ι] :
                    (⨅ (i : ι), Filter.principal (s i)).HasBasis (fun (x : ι) => True) s
                    theorem Filter.hasBasis_iInf_principal_finite {α : Type u_1} {ι : Type u_6} (s : ιSet α) :
                    (⨅ (i : ι), Filter.principal (s i)).HasBasis (fun (t : Set ι) => t.Finite) fun (t : Set ι) => it, 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 (x1 x2 : Set α) => x1 x2) S) (ne : S.Nonempty) :
                    (⨅ iS, Filter.principal (s i)).HasBasis (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) :
                    (⨅ (i : ι), ⨅ (_ : p i), Filter.principal (s i)).HasBasis p s
                    theorem Filter.HasBasis.map {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} (f : αβ) (hl : l.HasBasis p s) :
                    (Filter.map f l).HasBasis 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 : l.HasBasis p s) :
                    (Filter.comap f l).HasBasis p fun (i : ι) => f ⁻¹' s i
                    theorem Filter.comap_hasBasis {α : Type u_1} {β : Type u_2} (f : αβ) (l : Filter β) :
                    (Filter.comap f l).HasBasis (fun (s : Set β) => s l) fun (s : Set β) => f ⁻¹' s
                    theorem Filter.HasBasis.forall_mem_mem {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} (h : l.HasBasis p s) {x : α} :
                    (∀ tl, x t) ∀ (i : ι), p ix 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 : l.HasBasis p s) (hf : Monotone f) :
                    tl, f t = ⨅ (i : ι), ⨅ (_ : 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 : l.HasBasis p s) (hf : Monotone f) :
                    tl, f t = ⋂ (i : ι), ⋂ (_ : p i), f (s i)
                    theorem Filter.HasBasis.ker {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ιProp} {s : ιSet α} (h : l.HasBasis p s) :
                    l.ker = ⋂ (i : ι), ⋂ (_ : p i), s i
                    structure Filter.IsAntitoneBasis {α : Type u_1} {ι'' : Type u_6} [Preorder ι''] (s'' : ι''Set α) extends Filter.IsBasis :

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

                    • nonempty : ∃ (i : ι''), True
                    • inter : ∀ {i j : ι''}, TrueTrue∃ (k : ι''), True s'' k s'' i s'' j
                    • antitone : Antitone s''

                      The sequence of sets is antitone.

                    Instances For
                      theorem Filter.IsAntitoneBasis.antitone {α : Type u_1} {ι'' : Type u_6} [Preorder ι''] {s'' : ι''Set α} (self : Filter.IsAntitoneBasis s'') :

                      The sequence of sets is antitone.

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

                      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.

                      Instances For
                        theorem Filter.HasAntitoneBasis.antitone {α : Type u_1} {ι'' : Type u_6} [Preorder ι''] {l : Filter α} {s : ι''Set α} (self : l.HasAntitoneBasis s) :

                        The sequence of sets is antitone.

                        theorem Filter.HasAntitoneBasis.map {α : Type u_1} {β : Type u_2} {ι'' : Type u_6} [Preorder ι''] {l : Filter α} {s : ι''Set α} (hf : l.HasAntitoneBasis s) (m : αβ) :
                        (Filter.map m l).HasAntitoneBasis fun (x : ι'') => m '' s x
                        theorem Filter.HasAntitoneBasis.comap {α : Type u_1} {β : Type u_2} {ι'' : Type u_6} [Preorder ι''] {l : Filter α} {s : ι''Set α} (hf : l.HasAntitoneBasis s) (m : βα) :
                        (Filter.comap m l).HasAntitoneBasis fun (x : ι'') => m ⁻¹' s x
                        theorem Filter.HasAntitoneBasis.iInf_principal {α : Type u_1} {ι : Type u_7} [Preorder ι] [Nonempty ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] {s : ιSet α} (hs : Antitone s) :
                        (⨅ (i : ι), Filter.principal (s i)).HasAntitoneBasis s
                        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 : la.HasBasis pa sa) :
                        Filter.Tendsto f la lb tlb, ∃ (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 : lb.HasBasis 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 : la.HasBasis pa sa) (hlb : lb.HasBasis pb sb) :
                        Filter.Tendsto f la lb ∀ (ib : ι'), pb ib∃ (ia : ι), pa ia xsa 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 : la.HasBasis 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 : lb.HasBasis 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 : la.HasBasis pa sa) (hlb : lb.HasBasis 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 : la.HasBasis pa sa) (hlb : lb.HasBasis pb sb) :
                        (la ×ˢ lb).HasBasis (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 : la.HasBasis pa sa) (hlb : lb.HasBasis pb sb) :
                        (la ×ˢ lb).HasBasis (fun (i : ι × ι') => pa i.1 pb i.2) fun (i : ι × ι') => sa i.1 ×ˢ sb i.2
                        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 : la.HasBasis p sa) (hlb : lb.HasBasis p sb) (h_dir : ∀ {i j : ι}, p ip j∃ (k : ι), p k sa k sa i sb k sb j) :
                        (la ×ˢ lb).HasBasis 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 : la.HasBasis p sa) (hlb : lb.HasBasis p sb) (hsa : MonotoneOn sa {i : ι | p i}) (hsb : MonotoneOn sb {i : ι | p i}) :
                        (la ×ˢ lb).HasBasis 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 : la.HasBasis p sa) (hlb : lb.HasBasis p sb) (hsa : AntitoneOn sa {i : ι | p i}) (hsb : AntitoneOn sb {i : ι | p i}) :
                        (la ×ˢ lb).HasBasis 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 : la.HasBasis pa sa) :
                        (la ×ˢ la).HasBasis pa fun (i : ι) => sa i ×ˢ sa i
                        theorem Filter.mem_prod_self_iff {α : Type u_1} {la : Filter α} {s : Set (α × α)} :
                        s la ×ˢ la tla, t ×ˢ t s
                        theorem Filter.eventually_prod_self_iff {α : Type u_1} {la : Filter α} {r : ααProp} :
                        (∀ᶠ (x : α × α) in la ×ˢ la, r x.1 x.2) tla, xt, yt, r x y
                        theorem Filter.HasAntitoneBasis.prod {α : Type u_1} {β : Type u_2} {ι : Type u_6} [LinearOrder ι] {f : Filter α} {g : Filter β} {s : ιSet α} {t : ιSet β} (hf : f.HasAntitoneBasis s) (hg : g.HasAntitoneBasis t) :
                        (f ×ˢ g).HasAntitoneBasis 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 : la.HasBasis pa sa) (hlb : lb.HasBasis pb sb) :
                        (la.coprod lb).HasBasis (fun (i : ι × ι') => pa i.1 pb i.2) fun (i : ι × ι') => Prod.fst ⁻¹' sa i.1 Prod.snd ⁻¹' sb i.2
                        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))) :
                        class Filter.IsCountablyGenerated {α : Type u_1} (f : Filter α) :

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

                        Instances
                          theorem Filter.IsCountablyGenerated.out {α : Type u_1} {f : Filter α} [self : f.IsCountablyGenerated] :
                          ∃ (s : Set (Set α)), s.Countable f = Filter.generate s

                          There exists a countable set that generates the filter.

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

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

                          • nonempty : ∃ (i : ι), p i
                          • inter : ∀ {i j : ι}, p ip j∃ (k : ι), p k s k s i s j
                          • countable : (setOf p).Countable

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

                          Instances For
                            theorem Filter.IsCountableBasis.countable {α : Type u_1} {ι : Type u_4} {p : ιProp} {s : ιSet α} (self : Filter.IsCountableBasis p s) :
                            (setOf p).Countable

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

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

                            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.

                            • mem_iff' : ∀ (t : Set α), t l ∃ (i : ι), p i s i t
                            • countable : (setOf p).Countable

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

                            Instances For
                              theorem Filter.HasCountableBasis.countable {α : Type u_1} {ι : Type u_4} {l : Filter α} {p : ιProp} {s : ιSet α} (self : l.HasCountableBasis p s) :
                              (setOf p).Countable

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

                              structure Filter.CountableFilterBasis (α : Type u_6) extends FilterBasis :
                              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.

                              • sets : Set (Set α)
                              • nonempty : self.sets.Nonempty
                              • inter_sets : ∀ {x y : Set α}, x self.setsy self.setszself.sets, z x y
                              • countable : self.sets.Countable

                                The set of sets of the filter basis is countable.

                              Instances For
                                theorem Filter.CountableFilterBasis.countable {α : Type u_6} (self : Filter.CountableFilterBasis α) :
                                self.sets.Countable

                                The set of sets of the filter basis is countable.

                                theorem Filter.HasCountableBasis.isCountablyGenerated {α : Type u_1} {ι : Type u_4} {f : Filter α} {p : ιProp} {s : ιSet α} (h : f.HasCountableBasis p s) :
                                f.IsCountablyGenerated
                                theorem Filter.HasBasis.isCountablyGenerated {α : Type u_1} {ι : Type u_4} [Countable ι] {f : Filter α} {p : ιProp} {s : ιSet α} (h : f.HasBasis p s) :
                                f.IsCountablyGenerated
                                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)
                                theorem Filter.countable_biInf_eq_iInf_seq {α : Type u_1} {ι : Type u_4} [CompleteLattice α] {B : Set ι} (Bcbl : B.Countable) (Bne : B.Nonempty) (f : ια) :
                                ∃ (x : ι), tB, f t = ⨅ (i : ), f (x i)
                                theorem Filter.countable_biInf_eq_iInf_seq' {α : Type u_1} {ι : Type u_4} [CompleteLattice α] {B : Set ι} (Bcbl : B.Countable) (f : ια) {i₀ : ι} (h : f i₀ = ) :
                                ∃ (x : ι), tB, f t = ⨅ (i : ), f (x i)
                                theorem Filter.countable_biInf_principal_eq_seq_iInf {α : Type u_1} {B : Set (Set α)} (Bcbl : B.Countable) :
                                ∃ (x : Set α), tB, 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 : l.HasAntitoneBasis 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 : l.HasAntitoneBasis s) (i : ι) :
                                s i l
                                theorem Filter.HasAntitoneBasis.hasBasis_ge {α : Type u_1} {ι : Type u_4} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 x2] {l : Filter α} {s : ιSet α} (hs : l.HasAntitoneBasis s) (i : ι) :
                                l.HasBasis (fun (j : ι) => i j) s
                                theorem Filter.HasBasis.exists_antitone_subbasis {α : Type u_1} {ι' : Sort u_5} {f : Filter α} [h : f.IsCountablyGenerated] {p : ι'Prop} {s : ι'Set α} (hs : f.HasBasis p s) :
                                ∃ (x : ι'), (∀ (i : ), p (x i)) f.HasAntitoneBasis 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 α) [f.IsCountablyGenerated] :
                                ∃ (x : Set α), f.HasAntitoneBasis 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 α) [f.IsCountablyGenerated] :
                                ∃ (x : Set α), Antitone x ∀ {s : Set α}, s f ∃ (i : ), x i s
                                instance Filter.Inf.isCountablyGenerated {α : Type u_1} (f : Filter α) (g : Filter α) [f.IsCountablyGenerated] [g.IsCountablyGenerated] :
                                (f g).IsCountablyGenerated
                                Equations
                                • =
                                instance Filter.map.isCountablyGenerated {α : Type u_1} {β : Type u_2} (l : Filter α) [l.IsCountablyGenerated] (f : αβ) :
                                (Filter.map f l).IsCountablyGenerated
                                Equations
                                • =
                                instance Filter.comap.isCountablyGenerated {α : Type u_1} {β : Type u_2} (l : Filter β) [l.IsCountablyGenerated] (f : αβ) :
                                (Filter.comap f l).IsCountablyGenerated
                                Equations
                                • =
                                instance Filter.Sup.isCountablyGenerated {α : Type u_1} (f : Filter α) (g : Filter α) [f.IsCountablyGenerated] [g.IsCountablyGenerated] :
                                (f g).IsCountablyGenerated
                                Equations
                                • =
                                instance Filter.prod.isCountablyGenerated {α : Type u_1} {β : Type u_2} (la : Filter α) (lb : Filter β) [la.IsCountablyGenerated] [lb.IsCountablyGenerated] :
                                (la ×ˢ lb).IsCountablyGenerated
                                Equations
                                • =
                                instance Filter.coprod.isCountablyGenerated {α : Type u_1} {β : Type u_2} (la : Filter α) (lb : Filter β) [la.IsCountablyGenerated] [lb.IsCountablyGenerated] :
                                (la.coprod lb).IsCountablyGenerated
                                Equations
                                • =
                                theorem Filter.isCountablyGenerated_seq {α : Type u_1} {ι' : Sort u_5} [Countable ι'] (x : ι'Set α) :
                                (⨅ (i : ι'), Filter.principal (x i)).IsCountablyGenerated
                                theorem Filter.isCountablyGenerated_of_seq {α : Type u_1} {f : Filter α} (h : ∃ (x : Set α), f = ⨅ (i : ), Filter.principal (x i)) :
                                f.IsCountablyGenerated
                                theorem Filter.isCountablyGenerated_biInf_principal {α : Type u_1} {B : Set (Set α)} (h : B.Countable) :
                                (⨅ sB, Filter.principal s).IsCountablyGenerated
                                theorem Filter.isCountablyGenerated_iff_exists_antitone_basis {α : Type u_1} {f : Filter α} :
                                f.IsCountablyGenerated ∃ (x : Set α), f.HasAntitoneBasis x
                                theorem Filter.isCountablyGenerated_principal {α : Type u_1} (s : Set α) :
                                (Filter.principal s).IsCountablyGenerated
                                theorem Filter.isCountablyGenerated_pure {α : Type u_1} (a : α) :
                                (pure a).IsCountablyGenerated
                                theorem Filter.isCountablyGenerated_bot {α : Type u_1} :
                                .IsCountablyGenerated
                                theorem Filter.isCountablyGenerated_top {α : Type u_1} :
                                .IsCountablyGenerated
                                instance Filter.iInf.isCountablyGenerated {ι : Sort u} {α : Type v} [Countable ι] (f : ιFilter α) [∀ (i : ι), (f i).IsCountablyGenerated] :
                                (⨅ (i : ι), f i).IsCountablyGenerated
                                Equations
                                • =