Documentation

Mathlib.Order.Filter.Basic

Theory of filters on sets #

A filter on a type α is a collection of sets of α which contains the whole α, is upwards-closed, and is stable under intersection. They are mostly used to abstract two related kinds of ideas:

Main definitions #

In this file, we endow Filter α it with a complete lattice structure. This structure is lifted from the lattice structure on Set (Set X) using the Galois insertion which maps a filter to its elements in one direction, and an arbitrary set of sets to the smallest filter containing it in the other direction. We also prove Filter is a monadic functor, with a push-forward operation Filter.map and a pull-back operation Filter.comap that form a Galois connections for the order on filters.

The examples of filters appearing in the description of the two motivating ideas are:

The general notion of limit of a map with respect to filters on the source and target types is Filter.Tendsto. It is defined in terms of the order and the push-forward operation. The predicate "happening eventually" is Filter.Eventually, and "happening often" is Filter.Frequently, whose definitions are immediate after Filter is defined (but they come rather late in this file in order to immediately relate them to the lattice structure).

For instance, anticipating on Topology.Basic, the statement: "if a sequence u converges to some x and u n belongs to a set M for n large enough then x is in the closure of M" is formalized as: Tendsto u atTop (𝓝 x) → (∀ᶠ n in atTop, u n ∈ M) → x ∈ closure M, which is a special case of mem_closure_of_tendsto from Topology.Basic.

Notations #

References #

Important note: Bourbaki requires that a filter on X cannot contain all sets of X, which we do not require. This gives Filter X better formal properties, in particular a bottom element for its lattice structure, at the cost of including the assumption [NeBot f] in a number of lemmas and definitions.

instance Filter.inhabitedMem {α : Type u} {f : Filter α} :
Inhabited { s : Set α // s f }
Equations
  • Filter.inhabitedMem = { default := Set.univ, }
theorem Filter.filter_eq_iff {α : Type u} {f : Filter α} {g : Filter α} :
f = g f.sets = g.sets
theorem Filter.coext {α : Type u} {f : Filter α} {g : Filter α} (h : ∀ (s : Set α), s f s g) :
f = g

An extensionality lemma that is useful for filters with good lemmas about sᶜ ∈ f (e.g., Filter.comap, Filter.coprod, Filter.Coprod, Filter.cofinite).

instance Filter.instTransSetSupersetMem {α : Type u} :
Trans (fun (x1 x2 : Set α) => x1 x2) (fun (x1 : Set α) (x2 : Filter α) => x1 x2) fun (x1 : Set α) (x2 : Filter α) => x1 x2
Equations
  • Filter.instTransSetSupersetMem = { trans := }
instance Filter.instTransSetMemSubset {α : Type u} :
Trans Membership.mem (fun (x1 x2 : Set α) => x1 x2) Membership.mem
Equations
  • Filter.instTransSetMemSubset = { trans := }
@[simp]
theorem Filter.inter_mem_iff {α : Type u} {f : Filter α} {s : Set α} {t : Set α} :
s t f s f t f
theorem Filter.diff_mem {α : Type u} {f : Filter α} {s : Set α} {t : Set α} (hs : s f) (ht : t f) :
s \ t f
theorem Filter.congr_sets {α : Type u} {f : Filter α} {s : Set α} {t : Set α} (h : {x : α | x s x t} f) :
s f t f
theorem Filter.copy_eq {α : Type u} {f : Filter α} {S : Set (Set α)} (hmem : ∀ (s : Set α), s S s f) :
f.copy S hmem = f
@[simp]
theorem Filter.biInter_mem {α : Type u} {f : Filter α} {β : Type v} {s : βSet α} {is : Set β} (hf : is.Finite) :
iis, s i f iis, s i f
@[simp]
theorem Filter.biInter_finset_mem {α : Type u} {f : Filter α} {β : Type v} {s : βSet α} (is : Finset β) :
iis, s i f iis, s i f
theorem Finset.iInter_mem_sets {α : Type u} {f : Filter α} {β : Type v} {s : βSet α} (is : Finset β) :
iis, s i f iis, s i f

Alias of Filter.biInter_finset_mem.

@[simp]
theorem Filter.sInter_mem {α : Type u} {f : Filter α} {s : Set (Set α)} (hfin : s.Finite) :
⋂₀ s f Us, U f
@[simp]
theorem Filter.iInter_mem {α : Type u} {f : Filter α} {β : Sort v} {s : βSet α} [Finite β] :
⋂ (i : β), s i f ∀ (i : β), s i f
theorem Filter.exists_mem_subset_iff {α : Type u} {f : Filter α} {s : Set α} :
(∃ tf, t s) s f
theorem Filter.monotone_mem {α : Type u} {f : Filter α} :
Monotone fun (s : Set α) => s f
theorem Filter.exists_mem_and_iff {α : Type u} {f : Filter α} {P : Set αProp} {Q : Set αProp} (hP : Antitone P) (hQ : Antitone Q) :
((∃ uf, P u) uf, Q u) uf, P u Q u
theorem Filter.forall_in_swap {α : Type u} {f : Filter α} {β : Type u_1} {p : Set αβProp} :
(∀ af, ∀ (b : β), p a b) ∀ (b : β), af, p a b
theorem Filter.not_le {α : Type u} {f : Filter α} {g : Filter α} :
¬f g sg, sf
inductive Filter.GenerateSets {α : Type u} (g : Set (Set α)) :
Set αProp

GenerateSets g s: s is in the filter closure of g.

Instances For
    def Filter.generate {α : Type u} (g : Set (Set α)) :

    generate g is the largest filter containing the sets g.

    Equations
    Instances For
      theorem Filter.mem_generate_of_mem {α : Type u} {s : Set (Set α)} {U : Set α} (h : U s) :
      theorem Filter.le_generate_iff {α : Type u} {s : Set (Set α)} {f : Filter α} :
      f Filter.generate s s f.sets
      theorem Filter.mem_generate_iff {α : Type u} {s : Set (Set α)} {U : Set α} :
      U Filter.generate s ts, t.Finite ⋂₀ t U
      def Filter.mkOfClosure {α : Type u} (s : Set (Set α)) (hs : (Filter.generate s).sets = s) :

      mkOfClosure s hs constructs a filter on α whose elements set is exactly s : Set (Set α), provided one gives the assumption hs : (generate s).sets = s.

      Equations
      • Filter.mkOfClosure s hs = { sets := s, univ_sets := , sets_of_superset := , inter_sets := }
      Instances For
        theorem Filter.mkOfClosure_sets {α : Type u} {s : Set (Set α)} {hs : (Filter.generate s).sets = s} :
        def Filter.giGenerate (α : Type u_2) :
        GaloisInsertion Filter.generate Filter.sets

        Galois insertion from sets of sets into filters.

        Equations
        Instances For
          theorem Filter.mem_inf_iff {α : Type u} {f : Filter α} {g : Filter α} {s : Set α} :
          s f g t₁f, t₂g, s = t₁ t₂
          theorem Filter.mem_inf_of_left {α : Type u} {f : Filter α} {g : Filter α} {s : Set α} (h : s f) :
          s f g
          theorem Filter.mem_inf_of_right {α : Type u} {f : Filter α} {g : Filter α} {s : Set α} (h : s g) :
          s f g
          theorem Filter.inter_mem_inf {α : Type u} {f : Filter α} {g : Filter α} {s : Set α} {t : Set α} (hs : s f) (ht : t g) :
          s t f g
          theorem Filter.mem_inf_of_inter {α : Type u} {f : Filter α} {g : Filter α} {s : Set α} {t : Set α} {u : Set α} (hs : s f) (ht : t g) (h : s t u) :
          u f g
          theorem Filter.mem_inf_iff_superset {α : Type u} {f : Filter α} {g : Filter α} {s : Set α} :
          s f g t₁f, t₂g, t₁ t₂ s
          Equations
          instance Filter.instInhabited {α : Type u} :
          Equations
          • Filter.instInhabited = { default := }
          theorem Filter.NeBot.ne {α : Type u} {f : Filter α} (hf : f.NeBot) :
          @[simp]
          theorem Filter.not_neBot {α : Type u} {f : Filter α} :
          ¬f.NeBot f =
          theorem Filter.NeBot.mono {α : Type u} {f : Filter α} {g : Filter α} (hf : f.NeBot) (hg : f g) :
          g.NeBot
          theorem Filter.neBot_of_le {α : Type u} {f : Filter α} {g : Filter α} [hf : f.NeBot] (hg : f g) :
          g.NeBot
          @[simp]
          theorem Filter.sup_neBot {α : Type u} {f : Filter α} {g : Filter α} :
          (f g).NeBot f.NeBot g.NeBot
          theorem Filter.not_disjoint_self_iff {α : Type u} {f : Filter α} :
          ¬Disjoint f f f.NeBot
          theorem Filter.bot_sets_eq {α : Type u} :
          .sets = Set.univ
          theorem Filter.eq_or_neBot {α : Type u} (f : Filter α) :
          f = f.NeBot

          Either f = ⊥ or Filter.NeBot f. This is a version of eq_or_ne that uses Filter.NeBot as the second alternative, to be used as an instance.

          theorem Filter.sup_sets_eq {α : Type u} {f : Filter α} {g : Filter α} :
          (f g).sets = f.sets g.sets
          theorem Filter.sSup_sets_eq {α : Type u} {s : Set (Filter α)} :
          (sSup s).sets = fs, f.sets
          theorem Filter.iSup_sets_eq {α : Type u} {ι : Sort x} {f : ιFilter α} :
          (iSup f).sets = ⋂ (i : ι), (f i).sets
          theorem Filter.generate_iUnion {α : Type u} {ι : Sort x} {s : ιSet (Set α)} :
          Filter.generate (⋃ (i : ι), s i) = ⨅ (i : ι), Filter.generate (s i)
          @[simp]
          theorem Filter.mem_sup {α : Type u} {f : Filter α} {g : Filter α} {s : Set α} :
          s f g s f s g
          theorem Filter.union_mem_sup {α : Type u} {f : Filter α} {g : Filter α} {s : Set α} {t : Set α} (hs : s f) (ht : t g) :
          s t f g
          @[simp]
          theorem Filter.mem_sSup {α : Type u} {x : Set α} {s : Set (Filter α)} :
          x sSup s fs, x f
          @[simp]
          theorem Filter.mem_iSup {α : Type u} {ι : Sort x} {x : Set α} {f : ιFilter α} :
          x iSup f ∀ (i : ι), x f i
          @[simp]
          theorem Filter.iSup_neBot {α : Type u} {ι : Sort x} {f : ιFilter α} :
          (⨆ (i : ι), f i).NeBot ∃ (i : ι), (f i).NeBot
          theorem Filter.iInf_eq_generate {α : Type u} {ι : Sort x} (s : ιFilter α) :
          iInf s = Filter.generate (⋃ (i : ι), (s i).sets)
          theorem Filter.mem_iInf_of_mem {α : Type u} {ι : Sort x} {f : ιFilter α} (i : ι) {s : Set α} (hs : s f i) :
          s ⨅ (i : ι), f i
          theorem Filter.mem_iInf_of_iInter {α : Type u} {ι : Type u_2} {s : ιFilter α} {U : Set α} {I : Set ι} (I_fin : I.Finite) {V : ISet α} (hV : ∀ (i : I), V i s i) (hU : ⋂ (i : I), V i U) :
          U ⨅ (i : ι), s i
          theorem Filter.mem_iInf {α : Type u} {ι : Type u_2} {s : ιFilter α} {U : Set α} :
          U ⨅ (i : ι), s i ∃ (I : Set ι), I.Finite ∃ (V : ISet α), (∀ (i : I), V i s i) U = ⋂ (i : I), V i
          theorem Filter.mem_iInf' {α : Type u} {ι : Type u_2} {s : ιFilter α} {U : Set α} :
          U ⨅ (i : ι), s i ∃ (I : Set ι), I.Finite ∃ (V : ιSet α), (∀ (i : ι), V i s i) (∀ iI, V i = Set.univ) U = iI, V i U = ⋂ (i : ι), V i
          theorem Filter.exists_iInter_of_mem_iInf {ι : Type u_2} {α : Type u_3} {f : ιFilter α} {s : Set α} (hs : s ⨅ (i : ι), f i) :
          ∃ (t : ιSet α), (∀ (i : ι), t i f i) s = ⋂ (i : ι), t i
          theorem Filter.mem_iInf_of_finite {ι : Type u_2} [Finite ι] {α : Type u_3} {f : ιFilter α} (s : Set α) :
          s ⨅ (i : ι), f i ∃ (t : ιSet α), (∀ (i : ι), t i f i) s = ⋂ (i : ι), t i
          @[simp]
          theorem Filter.le_principal_iff {α : Type u} {s : Set α} {f : Filter α} :
          theorem Filter.Iic_principal {α : Type u} (s : Set α) :
          Set.Iic (Filter.principal s) = {l : Filter α | s l}
          theorem Filter.principal_mono {α : Type u} {s : Set α} {t : Set α} :
          theorem GCongr.filter_principal_mono {α : Type u} {s : Set α} {t : Set α} :

          Alias of the reverse direction of Filter.principal_mono.

          theorem Filter.monotone_principal {α : Type u} :
          Monotone Filter.principal
          @[simp]
          theorem Filter.principal_eq_iff_eq {α : Type u} {s : Set α} {t : Set α} :
          @[simp]
          theorem Filter.join_principal_eq_sSup {α : Type u} {s : Set (Filter α)} :
          @[simp]
          theorem Filter.principal_univ {α : Type u} :
          theorem Filter.generate_eq_biInf {α : Type u} (S : Set (Set α)) :

          Lattice equations #

          theorem Filter.empty_mem_iff_bot {α : Type u} {f : Filter α} :
          theorem Filter.nonempty_of_mem {α : Type u} {f : Filter α} [hf : f.NeBot] {s : Set α} (hs : s f) :
          s.Nonempty
          theorem Filter.NeBot.nonempty_of_mem {α : Type u} {f : Filter α} (hf : f.NeBot) {s : Set α} (hs : s f) :
          s.Nonempty
          @[simp]
          theorem Filter.empty_not_mem {α : Type u} (f : Filter α) [f.NeBot] :
          f
          theorem Filter.nonempty_of_neBot {α : Type u} (f : Filter α) [f.NeBot] :
          theorem Filter.compl_not_mem {α : Type u} {f : Filter α} {s : Set α} [f.NeBot] (h : s f) :
          sf
          theorem Filter.filter_eq_bot_of_isEmpty {α : Type u} [IsEmpty α] (f : Filter α) :
          f =
          theorem Filter.disjoint_iff {α : Type u} {f : Filter α} {g : Filter α} :
          Disjoint f g sf, tg, Disjoint s t
          theorem Filter.disjoint_of_disjoint_of_mem {α : Type u} {f : Filter α} {g : Filter α} {s : Set α} {t : Set α} (h : Disjoint s t) (hs : s f) (ht : t g) :
          theorem Filter.NeBot.not_disjoint {α : Type u} {f : Filter α} {s : Set α} {t : Set α} (hf : f.NeBot) (hs : s f) (ht : t f) :
          theorem Filter.inf_eq_bot_iff {α : Type u} {f : Filter α} {g : Filter α} :
          f g = Uf, Vg, U V =
          theorem Pairwise.exists_mem_filter_of_disjoint {α : Type u} {ι : Type u_2} [Finite ι] {l : ιFilter α} (hd : Pairwise (Disjoint on l)) :
          ∃ (s : ιSet α), (∀ (i : ι), s i l i) Pairwise (Disjoint on s)
          theorem Set.PairwiseDisjoint.exists_mem_filter {α : Type u} {ι : Type u_2} {l : ιFilter α} {t : Set ι} (hd : t.PairwiseDisjoint l) (ht : t.Finite) :
          ∃ (s : ιSet α), (∀ (i : ι), s i l i) t.PairwiseDisjoint s
          instance Filter.unique {α : Type u} [IsEmpty α] :

          There is exactly one filter on an empty type.

          Equations
          • Filter.unique = { default := , uniq := }
          theorem Filter.NeBot.nonempty {α : Type u} (f : Filter α) [hf : f.NeBot] :
          theorem Filter.eq_top_of_neBot {α : Type u} [Subsingleton α] (l : Filter α) [l.NeBot] :
          l =

          There are only two filters on a Subsingleton: and . If the type is empty, then they are equal.

          theorem Filter.forall_mem_nonempty_iff_neBot {α : Type u} {f : Filter α} :
          (∀ sf, s.Nonempty) f.NeBot
          Equations
          • =
          theorem Filter.eq_sInf_of_mem_iff_exists_mem {α : Type u} {S : Set (Filter α)} {l : Filter α} (h : ∀ {s : Set α}, s l fS, s f) :
          l = sInf S
          theorem Filter.eq_iInf_of_mem_iff_exists_mem {α : Type u} {ι : Sort x} {f : ιFilter α} {l : Filter α} (h : ∀ {s : Set α}, s l ∃ (i : ι), s f i) :
          l = iInf f
          theorem Filter.eq_biInf_of_mem_iff_exists_mem {α : Type u} {ι : Sort x} {f : ιFilter α} {p : ιProp} {l : Filter α} (h : ∀ {s : Set α}, s l ∃ (i : ι), p i s f i) :
          l = ⨅ (i : ι), ⨅ (_ : p i), f i
          theorem Filter.iInf_sets_eq {α : Type u} {ι : Sort x} {f : ιFilter α} (h : Directed (fun (x1 x2 : Filter α) => x1 x2) f) [ne : Nonempty ι] :
          (iInf f).sets = ⋃ (i : ι), (f i).sets
          theorem Filter.mem_iInf_of_directed {α : Type u} {ι : Sort x} {f : ιFilter α} (h : Directed (fun (x1 x2 : Filter α) => x1 x2) f) [Nonempty ι] (s : Set α) :
          s iInf f ∃ (i : ι), s f i
          theorem Filter.mem_biInf_of_directed {α : Type u} {β : Type v} {f : βFilter α} {s : Set β} (h : DirectedOn (f ⁻¹'o fun (x1 x2 : Filter α) => x1 x2) s) (ne : s.Nonempty) {t : Set α} :
          t is, f i is, t f i
          theorem Filter.biInf_sets_eq {α : Type u} {β : Type v} {f : βFilter α} {s : Set β} (h : DirectedOn (f ⁻¹'o fun (x1 x2 : Filter α) => x1 x2) s) (ne : s.Nonempty) :
          (⨅ is, f i).sets = is, (f i).sets
          theorem Filter.iInf_sets_eq_finite {α : Type u} {ι : Type u_2} (f : ιFilter α) :
          (⨅ (i : ι), f i).sets = ⋃ (t : Finset ι), (⨅ it, f i).sets
          theorem Filter.iInf_sets_eq_finite' {α : Type u} {ι : Sort x} (f : ιFilter α) :
          (⨅ (i : ι), f i).sets = ⋃ (t : Finset (PLift ι)), (⨅ it, f i.down).sets
          theorem Filter.mem_iInf_finite {α : Type u} {ι : Type u_2} {f : ιFilter α} (s : Set α) :
          s iInf f ∃ (t : Finset ι), s it, f i
          theorem Filter.mem_iInf_finite' {α : Type u} {ι : Sort x} {f : ιFilter α} (s : Set α) :
          s iInf f ∃ (t : Finset (PLift ι)), s it, f i.down
          @[simp]
          theorem Filter.sup_join {α : Type u} {f₁ : Filter (Filter α)} {f₂ : Filter (Filter α)} :
          f₁.join f₂.join = (f₁ f₂).join
          @[simp]
          theorem Filter.iSup_join {α : Type u} {ι : Sort w} {f : ιFilter (Filter α)} :
          ⨆ (x : ι), (f x).join = (⨆ (x : ι), f x).join
          Equations
          @[reducible, inline]

          The dual version does not hold! Filter α is not a CompleteDistribLattice.

          Equations
          Instances For
            Equations
            theorem Filter.mem_iInf_finset {α : Type u} {β : Type v} {s : Finset α} {f : αFilter β} {t : Set β} :
            t as, f a ∃ (p : αSet β), (∀ as, p a f a) t = as, p a
            theorem Filter.iInf_neBot_of_directed' {α : Type u} {ι : Sort x} {f : ιFilter α} [Nonempty ι] (hd : Directed (fun (x1 x2 : Filter α) => x1 x2) f) :
            (∀ (i : ι), (f i).NeBot)(iInf f).NeBot

            If f : ι → Filter α is directed, ι is not empty, and ∀ i, f i ≠ ⊥, then iInf f ≠ ⊥. See also iInf_neBot_of_directed for a version assuming Nonempty α instead of Nonempty ι.

            theorem Filter.iInf_neBot_of_directed {α : Type u} {ι : Sort x} {f : ιFilter α} [hn : Nonempty α] (hd : Directed (fun (x1 x2 : Filter α) => x1 x2) f) (hb : ∀ (i : ι), (f i).NeBot) :
            (iInf f).NeBot

            If f : ι → Filter α is directed, α is not empty, and ∀ i, f i ≠ ⊥, then iInf f ≠ ⊥. See also iInf_neBot_of_directed' for a version assuming Nonempty ι instead of Nonempty α.

            theorem Filter.sInf_neBot_of_directed' {α : Type u} {s : Set (Filter α)} (hne : s.Nonempty) (hd : DirectedOn (fun (x1 x2 : Filter α) => x1 x2) s) (hbot : s) :
            (sInf s).NeBot
            theorem Filter.sInf_neBot_of_directed {α : Type u} [Nonempty α] {s : Set (Filter α)} (hd : DirectedOn (fun (x1 x2 : Filter α) => x1 x2) s) (hbot : s) :
            (sInf s).NeBot
            theorem Filter.iInf_neBot_iff_of_directed' {α : Type u} {ι : Sort x} {f : ιFilter α} [Nonempty ι] (hd : Directed (fun (x1 x2 : Filter α) => x1 x2) f) :
            (iInf f).NeBot ∀ (i : ι), (f i).NeBot
            theorem Filter.iInf_neBot_iff_of_directed {α : Type u} {ι : Sort x} {f : ιFilter α} [Nonempty α] (hd : Directed (fun (x1 x2 : Filter α) => x1 x2) f) :
            (iInf f).NeBot ∀ (i : ι), (f i).NeBot
            theorem Filter.iInf_sets_induct {α : Type u} {ι : Sort x} {f : ιFilter α} {s : Set α} (hs : s iInf f) {p : Set αProp} (uni : p Set.univ) (ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ f ip s₂p (s₁ s₂)) :
            p s

            principal equations #

            @[simp]
            @[simp]
            @[simp]
            theorem Filter.iSup_principal {α : Type u} {ι : Sort w} {s : ιSet α} :
            ⨆ (x : ι), Filter.principal (s x) = Filter.principal (⋃ (i : ι), s i)
            @[simp]
            @[simp]
            theorem Filter.principal_neBot_iff {α : Type u} {s : Set α} :
            (Filter.principal s).NeBot s.Nonempty
            theorem Set.Nonempty.principal_neBot {α : Type u} {s : Set α} :
            s.Nonempty(Filter.principal s).NeBot

            Alias of the reverse direction of Filter.principal_neBot_iff.

            theorem Filter.mem_inf_principal' {α : Type u} {f : Filter α} {s : Set α} {t : Set α} :
            theorem Filter.mem_inf_principal {α : Type u} {f : Filter α} {s : Set α} {t : Set α} :
            s f Filter.principal t {x : α | x tx s} f
            theorem Filter.iSup_inf_principal {α : Type u} {ι : Sort x} (f : ιFilter α) (s : Set α) :
            ⨆ (i : ι), f i Filter.principal s = (⨆ (i : ι), f i) Filter.principal s
            theorem Filter.inf_principal_eq_bot {α : Type u} {f : Filter α} {s : Set α} :
            theorem Filter.mem_of_eq_bot {α : Type u} {f : Filter α} {s : Set α} (h : f Filter.principal s = ) :
            s f
            theorem Filter.diff_mem_inf_principal_compl {α : Type u} {f : Filter α} {s : Set α} (hs : s f) (t : Set α) :
            theorem Filter.principal_le_iff {α : Type u} {s : Set α} {f : Filter α} :
            Filter.principal s f Vf, s V
            @[simp]
            theorem Filter.iInf_principal_finset {α : Type u} {ι : Type w} (s : Finset ι) (f : ιSet α) :
            is, Filter.principal (f i) = Filter.principal (⋂ is, f i)
            theorem Filter.iInf_principal {α : Type u} {ι : Sort w} [Finite ι] (f : ιSet α) :
            ⨅ (i : ι), Filter.principal (f i) = Filter.principal (⋂ (i : ι), f i)
            @[simp]
            theorem Filter.iInf_principal' {α : Type u} {ι : Type w} [Finite ι] (f : ιSet α) :
            ⨅ (i : ι), Filter.principal (f i) = Filter.principal (⋂ (i : ι), f i)

            A special case of iInf_principal that is safe to mark simp.

            theorem Filter.iInf_principal_finite {α : Type u} {ι : Type w} {s : Set ι} (hs : s.Finite) (f : ιSet α) :
            is, Filter.principal (f i) = Filter.principal (⋂ is, f i)
            theorem Filter.join_mono {α : Type u} {f₁ : Filter (Filter α)} {f₂ : Filter (Filter α)} (h : f₁ f₂) :
            f₁.join f₂.join

            Eventually #

            theorem Filter.eventually_iff {α : Type u} {f : Filter α} {P : αProp} :
            (∀ᶠ (x : α) in f, P x) {x : α | P x} f
            @[simp]
            theorem Filter.eventually_mem_set {α : Type u} {s : Set α} {l : Filter α} :
            (∀ᶠ (x : α) in l, x s) s l
            theorem Filter.ext' {α : Type u} {f₁ : Filter α} {f₂ : Filter α} (h : ∀ (p : αProp), (∀ᶠ (x : α) in f₁, p x) ∀ᶠ (x : α) in f₂, p x) :
            f₁ = f₂
            theorem Filter.Eventually.filter_mono {α : Type u} {f₁ : Filter α} {f₂ : Filter α} (h : f₁ f₂) {p : αProp} (hp : ∀ᶠ (x : α) in f₂, p x) :
            ∀ᶠ (x : α) in f₁, p x
            theorem Filter.eventually_of_mem {α : Type u} {f : Filter α} {P : αProp} {U : Set α} (hU : U f) (h : xU, P x) :
            ∀ᶠ (x : α) in f, P x
            theorem Filter.Eventually.and {α : Type u} {p : αProp} {q : αProp} {f : Filter α} :
            Filter.Eventually p fFilter.Eventually q f∀ᶠ (x : α) in f, p x q x
            @[simp]
            theorem Filter.eventually_true {α : Type u} (f : Filter α) :
            ∀ᶠ (x : α) in f, True
            theorem Filter.Eventually.of_forall {α : Type u} {p : αProp} {f : Filter α} (hp : ∀ (x : α), p x) :
            ∀ᶠ (x : α) in f, p x
            @[deprecated Filter.Eventually.of_forall]
            theorem Filter.eventually_of_forall {α : Type u} {p : αProp} {f : Filter α} (hp : ∀ (x : α), p x) :
            ∀ᶠ (x : α) in f, p x

            Alias of Filter.Eventually.of_forall.

            @[simp]
            theorem Filter.eventually_false_iff_eq_bot {α : Type u} {f : Filter α} :
            (∀ᶠ (x : α) in f, False) f =
            @[simp]
            theorem Filter.eventually_const {α : Type u} {f : Filter α} [t : f.NeBot] {p : Prop} :
            (∀ᶠ (x : α) in f, p) p
            theorem Filter.eventually_iff_exists_mem {α : Type u} {p : αProp} {f : Filter α} :
            (∀ᶠ (x : α) in f, p x) vf, yv, p y
            theorem Filter.Eventually.exists_mem {α : Type u} {p : αProp} {f : Filter α} (hp : ∀ᶠ (x : α) in f, p x) :
            vf, yv, p y
            theorem Filter.Eventually.mp {α : Type u} {p : αProp} {q : αProp} {f : Filter α} (hp : ∀ᶠ (x : α) in f, p x) (hq : ∀ᶠ (x : α) in f, p xq x) :
            ∀ᶠ (x : α) in f, q x
            theorem Filter.Eventually.mono {α : Type u} {p : αProp} {q : αProp} {f : Filter α} (hp : ∀ᶠ (x : α) in f, p x) (hq : ∀ (x : α), p xq x) :
            ∀ᶠ (x : α) in f, q x
            theorem Filter.forall_eventually_of_eventually_forall {α : Type u} {β : Type v} {f : Filter α} {p : αβProp} (h : ∀ᶠ (x : α) in f, ∀ (y : β), p x y) (y : β) :
            ∀ᶠ (x : α) in f, p x y
            @[simp]
            theorem Filter.eventually_and {α : Type u} {p : αProp} {q : αProp} {f : Filter α} :
            (∀ᶠ (x : α) in f, p x q x) (∀ᶠ (x : α) in f, p x) ∀ᶠ (x : α) in f, q x
            theorem Filter.Eventually.congr {α : Type u} {f : Filter α} {p : αProp} {q : αProp} (h' : ∀ᶠ (x : α) in f, p x) (h : ∀ᶠ (x : α) in f, p x q x) :
            ∀ᶠ (x : α) in f, q x
            theorem Filter.eventually_congr {α : Type u} {f : Filter α} {p : αProp} {q : αProp} (h : ∀ᶠ (x : α) in f, p x q x) :
            (∀ᶠ (x : α) in f, p x) ∀ᶠ (x : α) in f, q x
            @[simp]
            theorem Filter.eventually_all {α : Type u} {ι : Sort u_2} [Finite ι] {l : Filter α} {p : ιαProp} :
            (∀ᶠ (x : α) in l, ∀ (i : ι), p i x) ∀ (i : ι), ∀ᶠ (x : α) in l, p i x
            @[simp]
            theorem Filter.eventually_all_finite {α : Type u} {ι : Type u_2} {I : Set ι} (hI : I.Finite) {l : Filter α} {p : ιαProp} :
            (∀ᶠ (x : α) in l, iI, p i x) iI, ∀ᶠ (x : α) in l, p i x
            theorem Set.Finite.eventually_all {α : Type u} {ι : Type u_2} {I : Set ι} (hI : I.Finite) {l : Filter α} {p : ιαProp} :
            (∀ᶠ (x : α) in l, iI, p i x) iI, ∀ᶠ (x : α) in l, p i x

            Alias of Filter.eventually_all_finite.

            @[simp]
            theorem Filter.eventually_all_finset {α : Type u} {ι : Type u_2} (I : Finset ι) {l : Filter α} {p : ιαProp} :
            (∀ᶠ (x : α) in l, iI, p i x) iI, ∀ᶠ (x : α) in l, p i x
            theorem Finset.eventually_all {α : Type u} {ι : Type u_2} (I : Finset ι) {l : Filter α} {p : ιαProp} :
            (∀ᶠ (x : α) in l, iI, p i x) iI, ∀ᶠ (x : α) in l, p i x

            Alias of Filter.eventually_all_finset.

            @[simp]
            theorem Filter.eventually_or_distrib_left {α : Type u} {f : Filter α} {p : Prop} {q : αProp} :
            (∀ᶠ (x : α) in f, p q x) p ∀ᶠ (x : α) in f, q x
            @[simp]
            theorem Filter.eventually_or_distrib_right {α : Type u} {f : Filter α} {p : αProp} {q : Prop} :
            (∀ᶠ (x : α) in f, p x q) (∀ᶠ (x : α) in f, p x) q
            theorem Filter.eventually_imp_distrib_left {α : Type u} {f : Filter α} {p : Prop} {q : αProp} :
            (∀ᶠ (x : α) in f, pq x) p∀ᶠ (x : α) in f, q x
            @[simp]
            theorem Filter.eventually_bot {α : Type u} {p : αProp} :
            ∀ᶠ (x : α) in , p x
            @[simp]
            theorem Filter.eventually_top {α : Type u} {p : αProp} :
            (∀ᶠ (x : α) in , p x) ∀ (x : α), p x
            @[simp]
            theorem Filter.eventually_sup {α : Type u} {p : αProp} {f : Filter α} {g : Filter α} :
            (∀ᶠ (x : α) in f g, p x) (∀ᶠ (x : α) in f, p x) ∀ᶠ (x : α) in g, p x
            @[simp]
            theorem Filter.eventually_sSup {α : Type u} {p : αProp} {fs : Set (Filter α)} :
            (∀ᶠ (x : α) in sSup fs, p x) ffs, ∀ᶠ (x : α) in f, p x
            @[simp]
            theorem Filter.eventually_iSup {α : Type u} {ι : Sort x} {p : αProp} {fs : ιFilter α} :
            (∀ᶠ (x : α) in ⨆ (b : ι), fs b, p x) ∀ (b : ι), ∀ᶠ (x : α) in fs b, p x
            @[simp]
            theorem Filter.eventually_principal {α : Type u} {a : Set α} {p : αProp} :
            (∀ᶠ (x : α) in Filter.principal a, p x) xa, p x
            theorem Filter.Eventually.forall_mem {α : Type u_2} {f : Filter α} {s : Set α} {P : αProp} (hP : ∀ᶠ (x : α) in f, P x) (hf : Filter.principal s f) (x : α) :
            x sP x
            theorem Filter.eventually_inf {α : Type u} {f : Filter α} {g : Filter α} {p : αProp} :
            (∀ᶠ (x : α) in f g, p x) sf, tg, xs t, p x
            theorem Filter.eventually_inf_principal {α : Type u} {f : Filter α} {p : αProp} {s : Set α} :
            (∀ᶠ (x : α) in f Filter.principal s, p x) ∀ᶠ (x : α) in f, x sp x

            Frequently #

            theorem Filter.Eventually.frequently {α : Type u} {f : Filter α} [f.NeBot] {p : αProp} (h : ∀ᶠ (x : α) in f, p x) :
            ∃ᶠ (x : α) in f, p x
            theorem Filter.Frequently.of_forall {α : Type u} {f : Filter α} [f.NeBot] {p : αProp} (h : ∀ (x : α), p x) :
            ∃ᶠ (x : α) in f, p x
            @[deprecated Filter.Frequently.of_forall]
            theorem Filter.frequently_of_forall {α : Type u} {f : Filter α} [f.NeBot] {p : αProp} (h : ∀ (x : α), p x) :
            ∃ᶠ (x : α) in f, p x

            Alias of Filter.Frequently.of_forall.

            theorem Filter.Frequently.mp {α : Type u} {p : αProp} {q : αProp} {f : Filter α} (h : ∃ᶠ (x : α) in f, p x) (hpq : ∀ᶠ (x : α) in f, p xq x) :
            ∃ᶠ (x : α) in f, q x
            theorem Filter.Frequently.filter_mono {α : Type u} {p : αProp} {f : Filter α} {g : Filter α} (h : ∃ᶠ (x : α) in f, p x) (hle : f g) :
            ∃ᶠ (x : α) in g, p x
            theorem Filter.Frequently.mono {α : Type u} {p : αProp} {q : αProp} {f : Filter α} (h : ∃ᶠ (x : α) in f, p x) (hpq : ∀ (x : α), p xq x) :
            ∃ᶠ (x : α) in f, q x
            theorem Filter.Frequently.and_eventually {α : Type u} {p : αProp} {q : αProp} {f : Filter α} (hp : ∃ᶠ (x : α) in f, p x) (hq : ∀ᶠ (x : α) in f, q x) :
            ∃ᶠ (x : α) in f, p x q x
            theorem Filter.Eventually.and_frequently {α : Type u} {p : αProp} {q : αProp} {f : Filter α} (hp : ∀ᶠ (x : α) in f, p x) (hq : ∃ᶠ (x : α) in f, q x) :
            ∃ᶠ (x : α) in f, p x q x
            theorem Filter.Frequently.exists {α : Type u} {p : αProp} {f : Filter α} (hp : ∃ᶠ (x : α) in f, p x) :
            ∃ (x : α), p x
            theorem Filter.Eventually.exists {α : Type u} {p : αProp} {f : Filter α} [f.NeBot] (hp : ∀ᶠ (x : α) in f, p x) :
            ∃ (x : α), p x
            theorem Filter.frequently_iff_neBot {α : Type u} {l : Filter α} {p : αProp} :
            (∃ᶠ (x : α) in l, p x) (l Filter.principal {x : α | p x}).NeBot
            theorem Filter.frequently_mem_iff_neBot {α : Type u} {l : Filter α} {s : Set α} :
            (∃ᶠ (x : α) in l, x s) (l Filter.principal s).NeBot
            theorem Filter.frequently_iff_forall_eventually_exists_and {α : Type u} {p : αProp} {f : Filter α} :
            (∃ᶠ (x : α) in f, p x) ∀ {q : αProp}, (∀ᶠ (x : α) in f, q x)∃ (x : α), p x q x
            theorem Filter.frequently_iff {α : Type u} {f : Filter α} {P : αProp} :
            (∃ᶠ (x : α) in f, P x) ∀ {U : Set α}, U fxU, P x
            @[simp]
            theorem Filter.not_eventually {α : Type u} {p : αProp} {f : Filter α} :
            (¬∀ᶠ (x : α) in f, p x) ∃ᶠ (x : α) in f, ¬p x
            @[simp]
            theorem Filter.not_frequently {α : Type u} {p : αProp} {f : Filter α} :
            (¬∃ᶠ (x : α) in f, p x) ∀ᶠ (x : α) in f, ¬p x
            @[simp]
            theorem Filter.frequently_true_iff_neBot {α : Type u} (f : Filter α) :
            (∃ᶠ (x : α) in f, True) f.NeBot
            @[simp]
            theorem Filter.frequently_false {α : Type u} (f : Filter α) :
            ¬∃ᶠ (x : α) in f, False
            @[simp]
            theorem Filter.frequently_const {α : Type u} {f : Filter α} [f.NeBot] {p : Prop} :
            (∃ᶠ (x : α) in f, p) p
            @[simp]
            theorem Filter.frequently_or_distrib {α : Type u} {f : Filter α} {p : αProp} {q : αProp} :
            (∃ᶠ (x : α) in f, p x q x) (∃ᶠ (x : α) in f, p x) ∃ᶠ (x : α) in f, q x
            theorem Filter.frequently_or_distrib_left {α : Type u} {f : Filter α} [f.NeBot] {p : Prop} {q : αProp} :
            (∃ᶠ (x : α) in f, p q x) p ∃ᶠ (x : α) in f, q x
            theorem Filter.frequently_or_distrib_right {α : Type u} {f : Filter α} [f.NeBot] {p : αProp} {q : Prop} :
            (∃ᶠ (x : α) in f, p x q) (∃ᶠ (x : α) in f, p x) q
            theorem Filter.frequently_imp_distrib {α : Type u} {f : Filter α} {p : αProp} {q : αProp} :
            (∃ᶠ (x : α) in f, p xq x) (∀ᶠ (x : α) in f, p x)∃ᶠ (x : α) in f, q x
            theorem Filter.frequently_imp_distrib_left {α : Type u} {f : Filter α} [f.NeBot] {p : Prop} {q : αProp} :
            (∃ᶠ (x : α) in f, pq x) p∃ᶠ (x : α) in f, q x
            theorem Filter.frequently_imp_distrib_right {α : Type u} {f : Filter α} [f.NeBot] {p : αProp} {q : Prop} :
            (∃ᶠ (x : α) in f, p xq) (∀ᶠ (x : α) in f, p x)q
            theorem Filter.eventually_imp_distrib_right {α : Type u} {f : Filter α} {p : αProp} {q : Prop} :
            (∀ᶠ (x : α) in f, p xq) (∃ᶠ (x : α) in f, p x)q
            @[simp]
            theorem Filter.frequently_and_distrib_left {α : Type u} {f : Filter α} {p : Prop} {q : αProp} :
            (∃ᶠ (x : α) in f, p q x) p ∃ᶠ (x : α) in f, q x
            @[simp]
            theorem Filter.frequently_and_distrib_right {α : Type u} {f : Filter α} {p : αProp} {q : Prop} :
            (∃ᶠ (x : α) in f, p x q) (∃ᶠ (x : α) in f, p x) q
            @[simp]
            theorem Filter.frequently_bot {α : Type u} {p : αProp} :
            ¬∃ᶠ (x : α) in , p x
            @[simp]
            theorem Filter.frequently_top {α : Type u} {p : αProp} :
            (∃ᶠ (x : α) in , p x) ∃ (x : α), p x
            @[simp]
            theorem Filter.frequently_principal {α : Type u} {a : Set α} {p : αProp} :
            (∃ᶠ (x : α) in Filter.principal a, p x) xa, p x
            theorem Filter.frequently_inf_principal {α : Type u} {f : Filter α} {s : Set α} {p : αProp} :
            (∃ᶠ (x : α) in f Filter.principal s, p x) ∃ᶠ (x : α) in f, x s p x
            theorem Filter.Frequently.inf_principal {α : Type u} {f : Filter α} {s : Set α} {p : αProp} :
            (∃ᶠ (x : α) in f, x s p x)∃ᶠ (x : α) in f Filter.principal s, p x

            Alias of the reverse direction of Filter.frequently_inf_principal.

            theorem Filter.Frequently.of_inf_principal {α : Type u} {f : Filter α} {s : Set α} {p : αProp} :
            (∃ᶠ (x : α) in f Filter.principal s, p x)∃ᶠ (x : α) in f, x s p x

            Alias of the forward direction of Filter.frequently_inf_principal.

            theorem Filter.frequently_sup {α : Type u} {p : αProp} {f : Filter α} {g : Filter α} :
            (∃ᶠ (x : α) in f g, p x) (∃ᶠ (x : α) in f, p x) ∃ᶠ (x : α) in g, p x
            @[simp]
            theorem Filter.frequently_sSup {α : Type u} {p : αProp} {fs : Set (Filter α)} :
            (∃ᶠ (x : α) in sSup fs, p x) ffs, ∃ᶠ (x : α) in f, p x
            @[simp]
            theorem Filter.frequently_iSup {α : Type u} {β : Type v} {p : αProp} {fs : βFilter α} :
            (∃ᶠ (x : α) in ⨆ (b : β), fs b, p x) ∃ (b : β), ∃ᶠ (x : α) in fs b, p x
            theorem Filter.Eventually.choice {α : Type u} {β : Type v} {r : αβProp} {l : Filter α} [l.NeBot] (h : ∀ᶠ (x : α) in l, ∃ (y : β), r x y) :
            ∃ (f : αβ), ∀ᶠ (x : α) in l, r x (f x)

            Relation “eventually equal” #

            theorem Filter.EventuallyEq.eventually {α : Type u} {β : Type v} {l : Filter α} {f : αβ} {g : αβ} (h : f =ᶠ[l] g) :
            ∀ᶠ (x : α) in l, f x = g x
            @[simp]
            theorem Filter.eventuallyEq_top {α : Type u} {β : Type v} {f : αβ} {g : αβ} :
            f =ᶠ[] g f = g
            theorem Filter.EventuallyEq.rw {α : Type u} {β : Type v} {l : Filter α} {f : αβ} {g : αβ} (h : f =ᶠ[l] g) (p : αβProp) (hf : ∀ᶠ (x : α) in l, p x (f x)) :
            ∀ᶠ (x : α) in l, p x (g x)
            theorem Filter.eventuallyEq_set {α : Type u} {s : Set α} {t : Set α} {l : Filter α} :
            s =ᶠ[l] t ∀ᶠ (x : α) in l, x s x t
            theorem Filter.EventuallyEq.mem_iff {α : Type u} {s : Set α} {t : Set α} {l : Filter α} :
            s =ᶠ[l] t∀ᶠ (x : α) in l, x s x t

            Alias of the forward direction of Filter.eventuallyEq_set.

            theorem Filter.Eventually.set_eq {α : Type u} {s : Set α} {t : Set α} {l : Filter α} :
            (∀ᶠ (x : α) in l, x s x t)s =ᶠ[l] t

            Alias of the reverse direction of Filter.eventuallyEq_set.

            @[simp]
            theorem Filter.eventuallyEq_univ {α : Type u} {s : Set α} {l : Filter α} :
            s =ᶠ[l] Set.univ s l
            theorem Filter.EventuallyEq.exists_mem {α : Type u} {β : Type v} {l : Filter α} {f : αβ} {g : αβ} (h : f =ᶠ[l] g) :
            sl, Set.EqOn f g s
            theorem Filter.eventuallyEq_of_mem {α : Type u} {β : Type v} {l : Filter α} {f : αβ} {g : αβ} {s : Set α} (hs : s l) (h : Set.EqOn f g s) :
            f =ᶠ[l] g
            theorem Filter.eventuallyEq_iff_exists_mem {α : Type u} {β : Type v} {l : Filter α} {f : αβ} {g : αβ} :
            f =ᶠ[l] g sl, Set.EqOn f g s
            theorem Filter.EventuallyEq.filter_mono {α : Type u} {β : Type v} {l : Filter α} {l' : Filter α} {f : αβ} {g : αβ} (h₁ : f =ᶠ[l] g) (h₂ : l' l) :
            f =ᶠ[l'] g
            @[simp]
            theorem Filter.EventuallyEq.refl {α : Type u} {β : Type v} (l : Filter α) (f : αβ) :
            f =ᶠ[l] f
            theorem Filter.EventuallyEq.rfl {α : Type u} {β : Type v} {l : Filter α} {f : αβ} :
            f =ᶠ[l] f
            theorem Filter.EventuallyEq.of_eq {α : Type u} {β : Type v} {l : Filter α} {f : αβ} {g : αβ} (h : f = g) :
            f =ᶠ[l] g
            theorem Eq.eventuallyEq {α : Type u} {β : Type v} {l : Filter α} {f : αβ} {g : αβ} (h : f = g) :
            f =ᶠ[l] g

            Alias of Filter.EventuallyEq.of_eq.

            theorem Filter.EventuallyEq.symm {α : Type u} {β : Type v} {f : αβ} {g : αβ} {l : Filter α} (H : f =ᶠ[l] g) :
            g =ᶠ[l] f
            theorem Filter.eventuallyEq_comm {α : Type u} {β : Type v} {f : αβ} {g : αβ} {l : Filter α} :
            f =ᶠ[l] g g =ᶠ[l] f
            theorem Filter.EventuallyEq.trans {α : Type u} {β : Type v} {l : Filter α} {f : αβ} {g : αβ} {h : αβ} (H₁ : f =ᶠ[l] g) (H₂ : g =ᶠ[l] h) :
            f =ᶠ[l] h
            theorem Filter.EventuallyEq.congr_left {α : Type u} {β : Type v} {l : Filter α} {f : αβ} {g : αβ} {h : αβ} (H : f =ᶠ[l] g) :
            f =ᶠ[l] h g =ᶠ[l] h
            theorem Filter.EventuallyEq.congr_right {α : Type u} {β : Type v} {l : Filter α} {f : αβ} {g : αβ} {h : αβ} (H : g =ᶠ[l] h) :
            f =ᶠ[l] g f =ᶠ[l] h
            instance Filter.instTransForallEventuallyEq {α : Type u} {β : Type v} {l : Filter α} :
            Trans (fun (x1 x2 : αβ) => x1 =ᶠ[l] x2) (fun (x1 x2 : αβ) => x1 =ᶠ[l] x2) fun (x1 x2 : αβ) => x1 =ᶠ[l] x2
            Equations
            • Filter.instTransForallEventuallyEq = { trans := }
            theorem Filter.EventuallyEq.prod_mk {α : Type u} {β : Type v} {γ : Type w} {l : Filter α} {f : αβ} {f' : αβ} (hf : f =ᶠ[l] f') {g : αγ} {g' : αγ} (hg : g =ᶠ[l] g') :
            (fun (x : α) => (f x, g x)) =ᶠ[l] fun (x : α) => (f' x, g' x)
            theorem Filter.EventuallyEq.fun_comp {α : Type u} {β : Type v} {γ : Type w} {f : αβ} {g : αβ} {l : Filter α} (H : f =ᶠ[l] g) (h : βγ) :
            h f =ᶠ[l] h g
            theorem Filter.EventuallyEq.comp₂ {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_2} {f : αβ} {f' : αβ} {g : αγ} {g' : αγ} {l : Filter α} (Hf : f =ᶠ[l] f') (h : βγδ) (Hg : g =ᶠ[l] g') :
            (fun (x : α) => h (f x) (g x)) =ᶠ[l] fun (x : α) => h (f' x) (g' x)
            theorem Filter.EventuallyEq.add {α : Type u} {β : Type v} [Add β] {f : αβ} {f' : αβ} {g : αβ} {g' : αβ} {l : Filter α} (h : f =ᶠ[l] g) (h' : f' =ᶠ[l] g') :
            (fun (x : α) => f x + f' x) =ᶠ[l] fun (x : α) => g x + g' x
            theorem Filter.EventuallyEq.mul {α : Type u} {β : Type v} [Mul β] {f : αβ} {f' : αβ} {g : αβ} {g' : αβ} {l : Filter α} (h : f =ᶠ[l] g) (h' : f' =ᶠ[l] g') :
            (fun (x : α) => f x * f' x) =ᶠ[l] fun (x : α) => g x * g' x
            theorem Filter.EventuallyEq.const_smul {α : Type u} {β : Type v} {γ : Type u_2} [SMul γ β] {f : αβ} {g : αβ} {l : Filter α} (h : f =ᶠ[l] g) (c : γ) :
            (fun (x : α) => c f x) =ᶠ[l] fun (x : α) => c g x
            theorem Filter.EventuallyEq.pow_const {α : Type u} {β : Type v} {γ : Type u_2} [Pow β γ] {f : αβ} {g : αβ} {l : Filter α} (h : f =ᶠ[l] g) (c : γ) :
            (fun (x : α) => f x ^ c) =ᶠ[l] fun (x : α) => g x ^ c
            theorem Filter.EventuallyEq.neg {α : Type u} {β : Type v} [Neg β] {f : αβ} {g : αβ} {l : Filter α} (h : f =ᶠ[l] g) :
            (fun (x : α) => -f x) =ᶠ[l] fun (x : α) => -g x
            theorem Filter.EventuallyEq.inv {α : Type u} {β : Type v} [Inv β] {f : αβ} {g : αβ} {l : Filter α} (h : f =ᶠ[l] g) :
            (fun (x : α) => (f x)⁻¹) =ᶠ[l] fun (x : α) => (g x)⁻¹
            theorem Filter.EventuallyEq.sub {α : Type u} {β : Type v} [Sub β] {f : αβ} {f' : αβ} {g : αβ} {g' : αβ} {l : Filter α} (h : f =ᶠ[l] g) (h' : f' =ᶠ[l] g') :
            (fun (x : α) => f x - f' x) =ᶠ[l] fun (x : α) => g x - g' x
            theorem Filter.EventuallyEq.div {α : Type u} {β : Type v} [Div β] {f : αβ} {f' : αβ} {g : αβ} {g' : αβ} {l : Filter α} (h : f =ᶠ[l] g) (h' : f' =ᶠ[l] g') :
            (fun (x : α) => f x / f' x) =ᶠ[l] fun (x : α) => g x / g' x
            theorem Filter.EventuallyEq.const_vadd {α : Type u} {β : Type v} {γ : Type u_2} [VAdd γ β] {f : αβ} {g : αβ} {l : Filter α} (h : f =ᶠ[l] g) (c : γ) :
            (fun (x : α) => c +ᵥ f x) =ᶠ[l] fun (x : α) => c +ᵥ g x
            theorem Filter.EventuallyEq.vadd {α : Type u} {β : Type v} {𝕜 : Type u_2} [VAdd 𝕜 β] {l : Filter α} {f : α𝕜} {f' : α𝕜} {g : αβ} {g' : αβ} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
            (fun (x : α) => f x +ᵥ g x) =ᶠ[l] fun (x : α) => f' x +ᵥ g' x
            theorem Filter.EventuallyEq.smul {α : Type u} {β : Type v} {𝕜 : Type u_2} [SMul 𝕜 β] {l : Filter α} {f : α𝕜} {f' : α𝕜} {g : αβ} {g' : αβ} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
            (fun (x : α) => f x g x) =ᶠ[l] fun (x : α) => f' x g' x
            theorem Filter.EventuallyEq.sup {α : Type u} {β : Type v} [Sup β] {l : Filter α} {f : αβ} {f' : αβ} {g : αβ} {g' : αβ} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
            (fun (x : α) => f x g x) =ᶠ[l] fun (x : α) => f' x g' x
            theorem Filter.EventuallyEq.inf {α : Type u} {β : Type v} [Inf β] {l : Filter α} {f : αβ} {f' : αβ} {g : αβ} {g' : αβ} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
            (fun (x : α) => f x g x) =ᶠ[l] fun (x : α) => f' x g' x
            theorem Filter.EventuallyEq.preimage {α : Type u} {β : Type v} {l : Filter α} {f : αβ} {g : αβ} (h : f =ᶠ[l] g) (s : Set β) :
            theorem Filter.EventuallyEq.inter {α : Type u} {s : Set α} {t : Set α} {s' : Set α} {t' : Set α} {l : Filter α} (h : s =ᶠ[l] t) (h' : s' =ᶠ[l] t') :
            s s' =ᶠ[l] t t'
            theorem Filter.EventuallyEq.union {α : Type u} {s : Set α} {t : Set α} {s' : Set α} {t' : Set α} {l : Filter α} (h : s =ᶠ[l] t) (h' : s' =ᶠ[l] t') :
            s s' =ᶠ[l] t t'
            theorem Filter.EventuallyEq.compl {α : Type u} {s : Set α} {t : Set α} {l : Filter α} (h : s =ᶠ[l] t) :
            theorem Filter.EventuallyEq.diff {α : Type u} {s : Set α} {t : Set α} {s' : Set α} {t' : Set α} {l : Filter α} (h : s =ᶠ[l] t) (h' : s' =ᶠ[l] t') :
            s \ s' =ᶠ[l] t \ t'
            theorem Filter.EventuallyEq.symmDiff {α : Type u} {s : Set α} {t : Set α} {s' : Set α} {t' : Set α} {l : Filter α} (h : s =ᶠ[l] t) (h' : s' =ᶠ[l] t') :
            theorem Filter.eventuallyEq_empty {α : Type u} {s : Set α} {l : Filter α} :
            s =ᶠ[l] ∀ᶠ (x : α) in l, xs
            theorem Filter.inter_eventuallyEq_left {α : Type u} {s : Set α} {t : Set α} {l : Filter α} :
            s t =ᶠ[l] s ∀ᶠ (x : α) in l, x sx t
            theorem Filter.inter_eventuallyEq_right {α : Type u} {s : Set α} {t : Set α} {l : Filter α} :
            s t =ᶠ[l] t ∀ᶠ (x : α) in l, x tx s
            @[simp]
            theorem Filter.eventuallyEq_principal {α : Type u} {β : Type v} {s : Set α} {f : αβ} {g : αβ} :
            theorem Filter.eventuallyEq_inf_principal_iff {α : Type u} {β : Type v} {F : Filter α} {s : Set α} {f : αβ} {g : αβ} :
            f =ᶠ[F Filter.principal s] g ∀ᶠ (x : α) in F, x sf x = g x
            theorem Filter.EventuallyEq.sub_eq {α : Type u} {β : Type v} [AddGroup β] {f : αβ} {g : αβ} {l : Filter α} (h : f =ᶠ[l] g) :
            f - g =ᶠ[l] 0
            theorem Filter.eventuallyEq_iff_sub {α : Type u} {β : Type v} [AddGroup β] {f : αβ} {g : αβ} {l : Filter α} :
            f =ᶠ[l] g f - g =ᶠ[l] 0
            theorem Filter.EventuallyLE.congr {α : Type u} {β : Type v} [LE β] {l : Filter α} {f : αβ} {f' : αβ} {g : αβ} {g' : αβ} (H : f ≤ᶠ[l] g) (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
            f' ≤ᶠ[l] g'
            theorem Filter.eventuallyLE_congr {α : Type u} {β : Type v} [LE β] {l : Filter α} {f : αβ} {f' : αβ} {g : αβ} {g' : αβ} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
            f ≤ᶠ[l] g f' ≤ᶠ[l] g'
            theorem Filter.EventuallyEq.le {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {f : αβ} {g : αβ} (h : f =ᶠ[l] g) :
            theorem Filter.EventuallyLE.refl {α : Type u} {β : Type v} [Preorder β] (l : Filter α) (f : αβ) :
            theorem Filter.EventuallyLE.rfl {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {f : αβ} :
            theorem Filter.EventuallyLE.trans {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {f : αβ} {g : αβ} {h : αβ} (H₁ : f ≤ᶠ[l] g) (H₂ : g ≤ᶠ[l] h) :
            instance Filter.instTransForallEventuallyLE {α : Type u} {β : Type v} [Preorder β] {l : Filter α} :
            Trans (fun (x1 x2 : αβ) => x1 ≤ᶠ[l] x2) (fun (x1 x2 : αβ) => x1 ≤ᶠ[l] x2) fun (x1 x2 : αβ) => x1 ≤ᶠ[l] x2
            Equations
            • Filter.instTransForallEventuallyLE = { trans := }
            theorem Filter.EventuallyEq.trans_le {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {f : αβ} {g : αβ} {h : αβ} (H₁ : f =ᶠ[l] g) (H₂ : g ≤ᶠ[l] h) :
            instance Filter.instTransForallEventuallyEqEventuallyLE {α : Type u} {β : Type v} [Preorder β] {l : Filter α} :
            Trans (fun (x1 x2 : αβ) => x1 =ᶠ[l] x2) (fun (x1 x2 : αβ) => x1 ≤ᶠ[l] x2) fun (x1 x2 : αβ) => x1 ≤ᶠ[l] x2
            Equations
            • Filter.instTransForallEventuallyEqEventuallyLE = { trans := }
            theorem Filter.EventuallyLE.trans_eq {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {f : αβ} {g : αβ} {h : αβ} (H₁ : f ≤ᶠ[l] g) (H₂ : g =ᶠ[l] h) :
            instance Filter.instTransForallEventuallyLEEventuallyEq {α : Type u} {β : Type v} [Preorder β] {l : Filter α} :
            Trans (fun (x1 x2 : αβ) => x1 ≤ᶠ[l] x2) (fun (x1 x2 : αβ) => x1 =ᶠ[l] x2) fun (x1 x2 : αβ) => x1 ≤ᶠ[l] x2
            Equations
            • Filter.instTransForallEventuallyLEEventuallyEq = { trans := }
            theorem Filter.EventuallyLE.antisymm {α : Type u} {β : Type v} [PartialOrder β] {l : Filter α} {f : αβ} {g : αβ} (h₁ : f ≤ᶠ[l] g) (h₂ : g ≤ᶠ[l] f) :
            f =ᶠ[l] g
            theorem Filter.eventuallyLE_antisymm_iff {α : Type u} {β : Type v} [PartialOrder β] {l : Filter α} {f : αβ} {g : αβ} :
            f =ᶠ[l] g f ≤ᶠ[l] g g ≤ᶠ[l] f
            theorem Filter.EventuallyLE.le_iff_eq {α : Type u} {β : Type v} [PartialOrder β] {l : Filter α} {f : αβ} {g : αβ} (h : f ≤ᶠ[l] g) :
            g ≤ᶠ[l] f g =ᶠ[l] f
            theorem Filter.Eventually.ne_of_lt {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {f : αβ} {g : αβ} (h : ∀ᶠ (x : α) in l, f x < g x) :
            ∀ᶠ (x : α) in l, f x g x
            theorem Filter.Eventually.ne_top_of_lt {α : Type u} {β : Type v} [PartialOrder β] [OrderTop β] {l : Filter α} {f : αβ} {g : αβ} (h : ∀ᶠ (x : α) in l, f x < g x) :
            ∀ᶠ (x : α) in l, f x
            theorem Filter.Eventually.lt_top_of_ne {α : Type u} {β : Type v} [PartialOrder β] [OrderTop β] {l : Filter α} {f : αβ} (h : ∀ᶠ (x : α) in l, f x ) :
            ∀ᶠ (x : α) in l, f x <
            theorem Filter.Eventually.lt_top_iff_ne_top {α : Type u} {β : Type v} [PartialOrder β] [OrderTop β] {l : Filter α} {f : αβ} :
            (∀ᶠ (x : α) in l, f x < ) ∀ᶠ (x : α) in l, f x
            theorem Filter.EventuallyLE.inter {α : Type u} {s : Set α} {t : Set α} {s' : Set α} {t' : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) (h' : s' ≤ᶠ[l] t') :
            s s' ≤ᶠ[l] t t'
            theorem Filter.EventuallyLE.union {α : Type u} {s : Set α} {t : Set α} {s' : Set α} {t' : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) (h' : s' ≤ᶠ[l] t') :
            s s' ≤ᶠ[l] t t'
            theorem Filter.EventuallyLE.iUnion {α : Type u} {ι : Sort x} {l : Filter α} [Finite ι] {s : ιSet α} {t : ιSet α} (h : ∀ (i : ι), s i ≤ᶠ[l] t i) :
            ⋃ (i : ι), s i ≤ᶠ[l] ⋃ (i : ι), t i
            theorem Filter.EventuallyEq.iUnion {α : Type u} {ι : Sort x} {l : Filter α} [Finite ι] {s : ιSet α} {t : ιSet α} (h : ∀ (i : ι), s i =ᶠ[l] t i) :
            ⋃ (i : ι), s i =ᶠ[l] ⋃ (i : ι), t i
            theorem Filter.EventuallyLE.iInter {α : Type u} {ι : Sort x} {l : Filter α} [Finite ι] {s : ιSet α} {t : ιSet α} (h : ∀ (i : ι), s i ≤ᶠ[l] t i) :
            ⋂ (i : ι), s i ≤ᶠ[l] ⋂ (i : ι), t i
            theorem Filter.EventuallyEq.iInter {α : Type u} {ι : Sort x} {l : Filter α} [Finite ι] {s : ιSet α} {t : ιSet α} (h : ∀ (i : ι), s i =ᶠ[l] t i) :
            ⋂ (i : ι), s i =ᶠ[l] ⋂ (i : ι), t i
            theorem Set.Finite.eventuallyLE_iUnion {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι} (hs : s.Finite) {f : ιSet α} {g : ιSet α} (hle : is, f i ≤ᶠ[l] g i) :
            is, f i ≤ᶠ[l] is, g i
            theorem Filter.EventuallyLE.biUnion {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι} (hs : s.Finite) {f : ιSet α} {g : ιSet α} (hle : is, f i ≤ᶠ[l] g i) :
            is, f i ≤ᶠ[l] is, g i

            Alias of Set.Finite.eventuallyLE_iUnion.

            theorem Set.Finite.eventuallyEq_iUnion {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι} (hs : s.Finite) {f : ιSet α} {g : ιSet α} (heq : is, f i =ᶠ[l] g i) :
            is, f i =ᶠ[l] is, g i
            theorem Filter.EventuallyEq.biUnion {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι} (hs : s.Finite) {f : ιSet α} {g : ιSet α} (heq : is, f i =ᶠ[l] g i) :
            is, f i =ᶠ[l] is, g i

            Alias of Set.Finite.eventuallyEq_iUnion.

            theorem Set.Finite.eventuallyLE_iInter {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι} (hs : s.Finite) {f : ιSet α} {g : ιSet α} (hle : is, f i ≤ᶠ[l] g i) :
            is, f i ≤ᶠ[l] is, g i
            theorem Filter.EventuallyLE.biInter {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι} (hs : s.Finite) {f : ιSet α} {g : ιSet α} (hle : is, f i ≤ᶠ[l] g i) :
            is, f i ≤ᶠ[l] is, g i

            Alias of Set.Finite.eventuallyLE_iInter.

            theorem Set.Finite.eventuallyEq_iInter {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι} (hs : s.Finite) {f : ιSet α} {g : ιSet α} (heq : is, f i =ᶠ[l] g i) :
            is, f i =ᶠ[l] is, g i
            theorem Filter.EventuallyEq.biInter {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι} (hs : s.Finite) {f : ιSet α} {g : ιSet α} (heq : is, f i =ᶠ[l] g i) :
            is, f i =ᶠ[l] is, g i

            Alias of Set.Finite.eventuallyEq_iInter.

            theorem Finset.eventuallyLE_iUnion {α : Type u} {l : Filter α} {ι : Type u_2} (s : Finset ι) {f : ιSet α} {g : ιSet α} (hle : is, f i ≤ᶠ[l] g i) :
            is, f i ≤ᶠ[l] is, g i
            theorem Finset.eventuallyEq_iUnion {α : Type u} {l : Filter α} {ι : Type u_2} (s : Finset ι) {f : ιSet α} {g : ιSet α} (heq : is, f i =ᶠ[l] g i) :
            is, f i =ᶠ[l] is, g i
            theorem Finset.eventuallyLE_iInter {α : Type u} {l : Filter α} {ι : Type u_2} (s : Finset ι) {f : ιSet α} {g : ιSet α} (hle : is, f i ≤ᶠ[l] g i) :
            is, f i ≤ᶠ[l] is, g i
            theorem Finset.eventuallyEq_iInter {α : Type u} {l : Filter α} {ι : Type u_2} (s : Finset ι) {f : ιSet α} {g : ιSet α} (heq : is, f i =ᶠ[l] g i) :
            is, f i =ᶠ[l] is, g i
            theorem Filter.EventuallyLE.compl {α : Type u} {s : Set α} {t : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) :
            theorem Filter.EventuallyLE.diff {α : Type u} {s : Set α} {t : Set α} {s' : Set α} {t' : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) (h' : t' ≤ᶠ[l] s') :
            s \ s' ≤ᶠ[l] t \ t'
            theorem Filter.EventuallyLE.sup {α : Type u} {β : Type v} [SemilatticeSup β] {l : Filter α} {f₁ : αβ} {f₂ : αβ} {g₁ : αβ} {g₂ : αβ} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) :
            f₁ g₁ ≤ᶠ[l] f₂ g₂
            theorem Filter.EventuallyLE.sup_le {α : Type u} {β : Type v} [SemilatticeSup β] {l : Filter α} {f : αβ} {g : αβ} {h : αβ} (hf : f ≤ᶠ[l] h) (hg : g ≤ᶠ[l] h) :
            f g ≤ᶠ[l] h
            theorem Filter.EventuallyLE.le_sup_of_le_left {α : Type u} {β : Type v} [SemilatticeSup β] {l : Filter α} {f : αβ} {g : αβ} {h : αβ} (hf : h ≤ᶠ[l] f) :
            h ≤ᶠ[l] f g
            theorem Filter.EventuallyLE.le_sup_of_le_right {α : Type u} {β : Type v} [SemilatticeSup β] {l : Filter α} {f : αβ} {g : αβ} {h : αβ} (hg : h ≤ᶠ[l] g) :
            h ≤ᶠ[l] f g
            theorem Filter.join_le {α : Type u} {f : Filter (Filter α)} {l : Filter α} (h : ∀ᶠ (m : Filter α) in f, m l) :
            f.join l

            Push-forwards, pull-backs, and the monad structure #

            @[simp]
            theorem Filter.map_principal {α : Type u} {β : Type v} {s : Set α} {f : αβ} :
            @[simp]
            theorem Filter.eventually_map {α : Type u} {β : Type v} {f : Filter α} {m : αβ} {P : βProp} :
            (∀ᶠ (b : β) in Filter.map m f, P b) ∀ᶠ (a : α) in f, P (m a)
            @[simp]
            theorem Filter.frequently_map {α : Type u} {β : Type v} {f : Filter α} {m : αβ} {P : βProp} :
            (∃ᶠ (b : β) in Filter.map m f, P b) ∃ᶠ (a : α) in f, P (m a)
            @[simp]
            theorem Filter.mem_map {α : Type u} {β : Type v} {f : Filter α} {m : αβ} {t : Set β} :
            theorem Filter.mem_map' {α : Type u} {β : Type v} {f : Filter α} {m : αβ} {t : Set β} :
            t Filter.map m f {x : α | m x t} f
            theorem Filter.image_mem_map {α : Type u} {β : Type v} {f : Filter α} {m : αβ} {s : Set α} (hs : s f) :
            m '' s Filter.map m f
            @[simp]
            theorem Filter.image_mem_map_iff {α : Type u} {β : Type v} {f : Filter α} {m : αβ} {s : Set α} (hf : Function.Injective m) :
            m '' s Filter.map m f s f
            theorem Filter.range_mem_map {α : Type u} {β : Type v} {f : Filter α} {m : αβ} :
            theorem Filter.mem_map_iff_exists_image {α : Type u} {β : Type v} {f : Filter α} {m : αβ} {t : Set β} :
            t Filter.map m f sf, m '' s t
            @[simp]
            theorem Filter.map_id {α : Type u} {f : Filter α} :
            Filter.map id f = f
            @[simp]
            theorem Filter.map_id' {α : Type u} {f : Filter α} :
            Filter.map (fun (x : α) => x) f = f
            @[simp]
            theorem Filter.map_compose {α : Type u} {β : Type v} {γ : Type w} {m : αβ} {m' : βγ} :
            @[simp]
            theorem Filter.map_map {α : Type u} {β : Type v} {γ : Type w} {f : Filter α} {m : αβ} {m' : βγ} :
            theorem Filter.map_congr {α : Type u} {β : Type v} {m₁ : αβ} {m₂ : αβ} {f : Filter α} (h : m₁ =ᶠ[f] m₂) :
            Filter.map m₁ f = Filter.map m₂ f

            If functions m₁ and m₂ are eventually equal at a filter f, then they map this filter to the same filter.

            theorem Filter.mem_comap' {α : Type u} {β : Type v} {f : αβ} {l : Filter β} {s : Set α} :
            s Filter.comap f l {y : β | ∀ ⦃x : α⦄, f x = yx s} l
            theorem Filter.mem_comap'' {α : Type u} {β : Type v} {f : αβ} {l : Filter β} {s : Set α} :
            theorem Filter.mem_comap_prod_mk {α : Type u} {β : Type v} {x : α} {s : Set β} {F : Filter (α × β)} :
            s Filter.comap (Prod.mk x) F {p : α × β | p.1 = xp.2 s} F

            RHS form is used, e.g., in the definition of UniformSpace.

            @[simp]
            theorem Filter.eventually_comap {α : Type u} {β : Type v} {f : αβ} {l : Filter β} {p : αProp} :
            (∀ᶠ (a : α) in Filter.comap f l, p a) ∀ᶠ (b : β) in l, ∀ (a : α), f a = bp a
            @[simp]
            theorem Filter.frequently_comap {α : Type u} {β : Type v} {f : αβ} {l : Filter β} {p : αProp} :
            (∃ᶠ (a : α) in Filter.comap f l, p a) ∃ᶠ (b : β) in l, ∃ (a : α), f a = b p a
            theorem Filter.mem_comap_iff_compl {α : Type u} {β : Type v} {f : αβ} {l : Filter β} {s : Set α} :
            theorem Filter.compl_mem_comap {α : Type u} {β : Type v} {f : αβ} {l : Filter β} {s : Set α} :
            def Filter.kernMap {α : Type u} {β : Type v} (m : αβ) (f : Filter α) :

            The analog of kernImage for filters. A set s belongs to Filter.kernMap m f if either of the following equivalent conditions hold.

            1. There exists a set t ∈ f such that s = kernImage m t. This is used as a definition.
            2. There exists a set t such that tᶜ ∈ f and sᶜ = m '' t, see Filter.mem_kernMap_iff_compl and Filter.compl_mem_kernMap.

            This definition because it gives a right adjoint to Filter.comap, and because it has a nice interpretation when working with co- filters (Filter.cocompact, Filter.cofinite, ...). For example, kernMap m (cocompact α) is the filter generated by the complements of the sets m '' K where K is a compact subset of α.

            Equations
            Instances For
              theorem Filter.mem_kernMap {α : Type u} {β : Type v} {m : αβ} {f : Filter α} {s : Set β} :
              s Filter.kernMap m f tf, Set.kernImage m t = s
              theorem Filter.mem_kernMap_iff_compl {α : Type u} {β : Type v} {m : αβ} {f : Filter α} {s : Set β} :
              s Filter.kernMap m f ∃ (t : Set α), t f m '' t = s
              theorem Filter.compl_mem_kernMap {α : Type u} {β : Type v} {m : αβ} {f : Filter α} {s : Set β} :
              s Filter.kernMap m f ∃ (t : Set α), t f m '' t = s
              theorem Filter.pure_sets {α : Type u} (a : α) :
              (pure a).sets = {s : Set α | a s}
              @[simp]
              theorem Filter.mem_pure {α : Type u} {a : α} {s : Set α} :
              s pure a a s
              @[simp]
              theorem Filter.eventually_pure {α : Type u} {a : α} {p : αProp} :
              (∀ᶠ (x : α) in pure a, p x) p a
              @[simp]
              theorem Filter.principal_singleton {α : Type u} (a : α) :
              @[simp]
              theorem Filter.map_pure {α : Type u} {β : Type v} (f : αβ) (a : α) :
              Filter.map f (pure a) = pure (f a)
              theorem Filter.pure_le_principal {α : Type u} {s : Set α} (a : α) :
              @[simp]
              theorem Filter.join_pure {α : Type u} (f : Filter α) :
              (pure f).join = f
              @[simp]
              theorem Filter.pure_bind {α : Type u} {β : Type v} (a : α) (m : αFilter β) :
              (pure a).bind m = m a
              theorem Filter.map_bind {γ : Type w} {α : Type u_2} {β : Type u_3} (m : βγ) (f : Filter α) (g : αFilter β) :
              Filter.map m (f.bind g) = f.bind (Filter.map m g)
              theorem Filter.bind_map {γ : Type w} {α : Type u_2} {β : Type u_3} (m : αβ) (f : Filter α) (g : βFilter γ) :
              (Filter.map m f).bind g = f.bind (g m)

              Filter as a Monad #

              In this section we define Filter.monad, a Monad structure on Filters. This definition is not an instance because its Seq projection is not equal to the Filter.seq function we use in the Applicative instance on Filter.

              The monad structure on filters.

              Equations
              Instances For
                Equations
                @[simp]
                theorem Filter.map_def {α : Type u_2} {β : Type u_2} (m : αβ) (f : Filter α) :
                m <$> f = Filter.map m f
                @[simp]
                theorem Filter.bind_def {α : Type u_2} {β : Type u_2} (f : Filter α) (m : αFilter β) :
                f >>= m = f.bind m

                map and comap equations #

                @[simp]
                theorem Filter.mem_comap {α : Type u} {β : Type v} {g : Filter β} {m : αβ} {s : Set α} :
                s Filter.comap m g tg, m ⁻¹' t s
                theorem Filter.preimage_mem_comap {α : Type u} {β : Type v} {g : Filter β} {m : αβ} {t : Set β} (ht : t g) :
                theorem Filter.Eventually.comap {α : Type u} {β : Type v} {g : Filter β} {p : βProp} (hf : ∀ᶠ (b : β) in g, p b) (f : αβ) :
                ∀ᶠ (a : α) in Filter.comap f g, p (f a)
                theorem Filter.comap_id {α : Type u} {f : Filter α} :
                theorem Filter.comap_id' {α : Type u} {f : Filter α} :
                Filter.comap (fun (x : α) => x) f = f
                theorem Filter.comap_const_of_not_mem {α : Type u} {β : Type v} {g : Filter β} {t : Set β} {x : β} (ht : t g) (hx : xt) :
                Filter.comap (fun (x_1 : α) => x) g =
                theorem Filter.comap_const_of_mem {α : Type u} {β : Type v} {g : Filter β} {x : β} (h : tg, x t) :
                Filter.comap (fun (x_1 : α) => x) g =
                theorem Filter.map_const {α : Type u} {β : Type v} {f : Filter α} [f.NeBot] {c : β} :
                Filter.map (fun (x : α) => c) f = pure c
                theorem Filter.comap_comap {α : Type u} {β : Type v} {γ : Type w} {f : Filter α} {m : γβ} {n : βα} :

                The variables in the following lemmas are used as in this diagram:

                    φ
                  α → β
                θ ↓   ↓ ψ
                  γ → δ
                    ρ
                
                theorem Filter.map_comm {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} {φ : αβ} {θ : αγ} {ψ : βδ} {ρ : γδ} (H : ψ φ = ρ θ) (F : Filter α) :
                theorem Filter.comap_comm {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} {φ : αβ} {θ : αγ} {ψ : βδ} {ρ : γδ} (H : ψ φ = ρ θ) (G : Filter δ) :
                theorem Function.Semiconj.filter_map {α : Type u} {β : Type v} {f : αβ} {ga : αα} {gb : ββ} (h : Function.Semiconj f ga gb) :
                theorem Function.Commute.filter_map {α : Type u} {f : αα} {g : αα} (h : Function.Commute f g) :
                theorem Function.Semiconj.filter_comap {α : Type u} {β : Type v} {f : αβ} {ga : αα} {gb : ββ} (h : Function.Semiconj f ga gb) :
                theorem Function.Commute.filter_comap {α : Type u} {f : αα} {g : αα} (h : Function.Commute f g) :
                theorem Function.LeftInverse.filter_map {α : Type u} {β : Type v} {f : αβ} {g : βα} (hfg : Function.LeftInverse g f) :
                theorem Function.LeftInverse.filter_comap {α : Type u} {β : Type v} {f : αβ} {g : βα} (hfg : Function.LeftInverse g f) :
                theorem Function.RightInverse.filter_map {α : Type u} {β : Type v} {f : αβ} {g : βα} (hfg : Function.RightInverse g f) :
                theorem Function.RightInverse.filter_comap {α : Type u} {β : Type v} {f : αβ} {g : βα} (hfg : Function.RightInverse g f) :
                theorem Set.LeftInvOn.filter_map_Iic {α : Type u} {β : Type v} {s : Set α} {f : αβ} {g : βα} (hfg : Set.LeftInvOn g f s) :
                theorem Set.RightInvOn.filter_map_Iic {α : Type u} {β : Type v} {t : Set β} {f : αβ} {g : βα} (hfg : Set.RightInvOn g f t) :
                @[simp]
                theorem Filter.comap_principal {α : Type u} {β : Type v} {m : αβ} {t : Set β} :
                theorem Filter.principal_subtype {α : Type u_2} (s : Set α) (t : Set s) :
                Filter.principal t = Filter.comap Subtype.val (Filter.principal (Subtype.val '' t))
                @[simp]
                theorem Filter.comap_pure {α : Type u} {β : Type v} {m : αβ} {b : β} :
                theorem Filter.map_le_iff_le_comap {α : Type u} {β : Type v} {f : Filter α} {g : Filter β} {m : αβ} :
                theorem Filter.gc_map_comap {α : Type u} {β : Type v} (m : αβ) :
                theorem Filter.comap_le_iff_le_kernMap {α : Type u} {β : Type v} {f : Filter α} {g : Filter β} {m : αβ} :
                theorem Filter.gc_comap_kernMap {α : Type u} {β : Type v} (m : αβ) :
                theorem Filter.kernMap_principal {α : Type u} {β : Type v} {m : αβ} {s : Set α} :
                theorem Filter.map_mono {α : Type u} {β : Type v} {m : αβ} :
                theorem Filter.comap_mono {α : Type u} {β : Type v} {m : αβ} :
                theorem GCongr.Filter.map_le_map {α : Type u} {β : Type v} {m : αβ} {F : Filter α} {G : Filter α} (h : F G) :

                Temporary lemma that we can tag with gcongr

                theorem GCongr.Filter.comap_le_comap {α : Type u} {β : Type v} {m : αβ} {F : Filter β} {G : Filter β} (h : F G) :

                Temporary lemma that we can tag with gcongr

                @[simp]
                theorem Filter.map_bot {α : Type u} {β : Type v} {m : αβ} :
                @[simp]
                theorem Filter.map_sup {α : Type u} {β : Type v} {f₁ : Filter α} {f₂ : Filter α} {m : αβ} :
                Filter.map m (f₁ f₂) = Filter.map m f₁ Filter.map m f₂
                @[simp]
                theorem Filter.map_iSup {α : Type u} {β : Type v} {ι : Sort x} {m : αβ} {f : ιFilter α} :
                Filter.map m (⨆ (i : ι), f i) = ⨆ (i : ι), Filter.map m (f i)
                @[simp]
                theorem Filter.map_top {α : Type u} {β : Type v} (f : αβ) :
                @[simp]
                theorem Filter.comap_top {α : Type u} {β : Type v} {m : αβ} :
                @[simp]
                theorem Filter.comap_inf {α : Type u} {β : Type v} {g₁ : Filter β} {g₂ : Filter β} {m : αβ} :
                Filter.comap m (g₁ g₂) = Filter.comap m g₁ Filter.comap m g₂
                @[simp]
                theorem Filter.comap_iInf {α : Type u} {β : Type v} {ι : Sort x} {m : αβ} {f : ιFilter β} :
                Filter.comap m (⨅ (i : ι), f i) = ⨅ (i : ι), Filter.comap m (f i)
                theorem Filter.le_comap_top {α : Type u} {β : Type v} (f : αβ) (l : Filter α) :
                theorem Filter.map_comap_le {α : Type u} {β : Type v} {g : Filter β} {m : αβ} :
                theorem Filter.le_comap_map {α : Type u} {β : Type v} {f : Filter α} {m : αβ} :
                @[simp]
                theorem Filter.comap_bot {α : Type u} {β : Type v} {m : αβ} :
                theorem Filter.neBot_of_comap {α : Type u} {β : Type v} {g : Filter β} {m : αβ} (h : (Filter.comap m g).NeBot) :
                g.NeBot
                theorem Filter.comap_inf_principal_range {α : Type u} {β : Type v} {g : Filter β} {m : αβ} :
                theorem Filter.disjoint_comap {α : Type u} {β : Type v} {g₁ : Filter β} {g₂ : Filter β} {m : αβ} (h : Disjoint g₁ g₂) :
                theorem Filter.comap_iSup {α : Type u} {β : Type v} {ι : Sort u_2} {f : ιFilter β} {m : αβ} :
                Filter.comap m (iSup f) = ⨆ (i : ι), Filter.comap m (f i)
                theorem Filter.comap_sSup {α : Type u} {β : Type v} {s : Set (Filter β)} {m : αβ} :
                Filter.comap m (sSup s) = fs, Filter.comap m f
                theorem Filter.comap_sup {α : Type u} {β : Type v} {g₁ : Filter β} {g₂ : Filter β} {m : αβ} :
                Filter.comap m (g₁ g₂) = Filter.comap m g₁ Filter.comap m g₂
                theorem Filter.map_comap {α : Type u} {β : Type v} (f : Filter β) (m : αβ) :
                theorem Filter.map_comap_setCoe_val {β : Type v} (f : Filter β) (s : Set β) :
                Filter.map Subtype.val (Filter.comap Subtype.val f) = f Filter.principal s
                theorem Filter.map_comap_of_mem {α : Type u} {β : Type v} {f : Filter β} {m : αβ} (hf : Set.range m f) :
                instance Filter.canLift {α : Type u} {β : Type v} (c : βα) (p : αProp) [CanLift α β c p] :
                CanLift (Filter α) (Filter β) (Filter.map c) fun (f : Filter α) => ∀ᶠ (x : α) in f, p x
                Equations
                • =
                theorem Filter.comap_le_comap_iff {α : Type u} {β : Type v} {f : Filter β} {g : Filter β} {m : αβ} (hf : Set.range m f) :
                theorem Filter.map_comap_of_surjective {α : Type u} {β : Type v} {f : αβ} (hf : Function.Surjective f) (l : Filter β) :
                theorem Filter.comap_injective {α : Type u} {β : Type v} {f : αβ} (hf : Function.Surjective f) :
                theorem Function.Surjective.filter_map_top {α : Type u} {β : Type v} {f : αβ} (hf : Function.Surjective f) :
                theorem Filter.subtype_coe_map_comap {α : Type u} (s : Set α) (f : Filter α) :
                Filter.map Subtype.val (Filter.comap Subtype.val f) = f Filter.principal s
                theorem Filter.image_mem_of_mem_comap {α : Type u} {β : Type v} {f : Filter α} {c : βα} (h : Set.range c f) {W : Set β} (W_in : W Filter.comap c f) :
                c '' W f
                theorem Filter.image_coe_mem_of_mem_comap {α : Type u} {f : Filter α} {U : Set α} (h : U f) {W : Set U} (W_in : W Filter.comap Subtype.val f) :
                Subtype.val '' W f
                theorem Filter.comap_map {α : Type u} {β : Type v} {f : Filter α} {m : αβ} (h : Function.Injective m) :
                theorem Filter.mem_comap_iff {α : Type u} {β : Type v} {f : Filter β} {m : αβ} (inj : Function.Injective m) (large : Set.range m f) {S : Set α} :
                S Filter.comap m f m '' S f
                theorem Filter.map_le_map_iff_of_injOn {α : Type u} {β : Type v} {l₁ : Filter α} {l₂ : Filter α} {f : αβ} {s : Set α} (h₁ : s l₁) (h₂ : s l₂) (hinj : Set.InjOn f s) :
                Filter.map f l₁ Filter.map f l₂ l₁ l₂
                theorem Filter.map_le_map_iff {α : Type u} {β : Type v} {f : Filter α} {g : Filter α} {m : αβ} (hm : Function.Injective m) :
                theorem Filter.map_eq_map_iff_of_injOn {α : Type u} {β : Type v} {f : Filter α} {g : Filter α} {m : αβ} {s : Set α} (hsf : s f) (hsg : s g) (hm : Set.InjOn m s) :
                theorem Filter.map_inj {α : Type u} {β : Type v} {f : Filter α} {g : Filter α} {m : αβ} (hm : Function.Injective m) :
                theorem Filter.map_injective {α : Type u} {β : Type v} {m : αβ} (hm : Function.Injective m) :
                theorem Filter.comap_neBot_iff {α : Type u} {β : Type v} {f : Filter β} {m : αβ} :
                (Filter.comap m f).NeBot tf, ∃ (a : α), m a t
                theorem Filter.comap_neBot {α : Type u} {β : Type v} {f : Filter β} {m : αβ} (hm : tf, ∃ (a : α), m a t) :
                (Filter.comap m f).NeBot
                theorem Filter.comap_neBot_iff_frequently {α : Type u} {β : Type v} {f : Filter β} {m : αβ} :
                (Filter.comap m f).NeBot ∃ᶠ (y : β) in f, y Set.range m
                theorem Filter.comap_neBot_iff_compl_range {α : Type u} {β : Type v} {f : Filter β} {m : αβ} :
                (Filter.comap m f).NeBot (Set.range m)f
                theorem Filter.comap_eq_bot_iff_compl_range {α : Type u} {β : Type v} {f : Filter β} {m : αβ} :
                theorem Filter.comap_surjective_eq_bot {α : Type u} {β : Type v} {f : Filter β} {m : αβ} (hm : Function.Surjective m) :
                theorem Filter.disjoint_comap_iff {α : Type u} {β : Type v} {g₁ : Filter β} {g₂ : Filter β} {m : αβ} (h : Function.Surjective m) :
                Disjoint (Filter.comap m g₁) (Filter.comap m g₂) Disjoint g₁ g₂
                theorem Filter.NeBot.comap_of_range_mem {α : Type u} {β : Type v} {f : Filter β} {m : αβ} :
                f.NeBotSet.range m f(Filter.comap m f).NeBot
                @[simp]
                theorem Filter.comap_fst_neBot_iff {α : Type u} {β : Type v} {f : Filter α} :
                (Filter.comap Prod.fst f).NeBot f.NeBot Nonempty β
                theorem Filter.comap_fst_neBot {α : Type u} {β : Type v} [Nonempty β] {f : Filter α} [f.NeBot] :
                (Filter.comap Prod.fst f).NeBot
                @[simp]
                theorem Filter.comap_snd_neBot_iff {α : Type u} {β : Type v} {f : Filter β} :
                (Filter.comap Prod.snd f).NeBot Nonempty α f.NeBot
                theorem Filter.comap_snd_neBot {α : Type u} {β : Type v} [Nonempty α] {f : Filter β} [f.NeBot] :
                (Filter.comap Prod.snd f).NeBot
                theorem Filter.comap_eval_neBot_iff' {ι : Type u_2} {α : ιType u_3} {i : ι} {f : Filter (α i)} :
                (Filter.comap (Function.eval i) f).NeBot (∀ (j : ι), Nonempty (α j)) f.NeBot
                @[simp]
                theorem Filter.comap_eval_neBot_iff {ι : Type u_2} {α : ιType u_3} [∀ (j : ι), Nonempty (α j)] {i : ι} {f : Filter (α i)} :
                (Filter.comap (Function.eval i) f).NeBot f.NeBot
                theorem Filter.comap_eval_neBot {ι : Type u_2} {α : ιType u_3} [∀ (j : ι), Nonempty (α j)] (i : ι) (f : Filter (α i)) [f.NeBot] :
                theorem Filter.comap_coe_neBot_of_le_principal {γ : Type w} {s : Set γ} {l : Filter γ} [h : l.NeBot] (h' : l Filter.principal s) :
                (Filter.comap Subtype.val l).NeBot
                theorem Filter.NeBot.comap_of_surj {α : Type u} {β : Type v} {f : Filter β} {m : αβ} (hf : f.NeBot) (hm : Function.Surjective m) :
                (Filter.comap m f).NeBot
                theorem Filter.NeBot.comap_of_image_mem {α : Type u} {β : Type v} {f : Filter β} {m : αβ} (hf : f.NeBot) {s : Set α} (hs : m '' s f) :
                (Filter.comap m f).NeBot
                @[simp]
                theorem Filter.map_eq_bot_iff {α : Type u} {β : Type v} {f : Filter α} {m : αβ} :
                theorem Filter.map_neBot_iff {α : Type u} {β : Type v} (f : αβ) {F : Filter α} :
                (Filter.map f F).NeBot F.NeBot
                theorem Filter.NeBot.map {α : Type u} {β : Type v} {f : Filter α} (hf : f.NeBot) (m : αβ) :
                (Filter.map m f).NeBot
                theorem Filter.NeBot.of_map {α : Type u} {β : Type v} {f : Filter α} {m : αβ} :
                (Filter.map m f).NeBotf.NeBot
                instance Filter.map_neBot {α : Type u} {β : Type v} {f : Filter α} {m : αβ} [hf : f.NeBot] :
                (Filter.map m f).NeBot
                Equations
                • =
                theorem Filter.sInter_comap_sets {α : Type u} {β : Type v} (f : αβ) (F : Filter β) :
                ⋂₀ (Filter.comap f F).sets = UF, f ⁻¹' U
                theorem Filter.map_iInf_le {α : Type u} {β : Type v} {ι : Sort x} {f : ιFilter α} {m : αβ} :
                Filter.map m (iInf f) ⨅ (i : ι), Filter.map m (f i)
                theorem Filter.map_iInf_eq {α : Type u} {β : Type v} {ι : Sort x} {f : ιFilter α} {m : αβ} (hf : Directed (fun (x1 x2 : Filter α) => x1 x2) f) [Nonempty ι] :
                Filter.map m (iInf f) = ⨅ (i : ι), Filter.map m (f i)
                theorem Filter.map_biInf_eq {α : Type u} {β : Type v} {ι : Type w} {f : ιFilter α} {m : αβ} {p : ιProp} (h : DirectedOn (f ⁻¹'o fun (x1 x2 : Filter α) => x1 x2) {x : ι | p x}) (ne : ∃ (i : ι), p i) :
                Filter.map m (⨅ (i : ι), ⨅ (_ : p i), f i) = ⨅ (i : ι), ⨅ (_ : p i), Filter.map m (f i)
                theorem Filter.map_inf_le {α : Type u} {β : Type v} {f : Filter α} {g : Filter α} {m : αβ} :
                theorem Filter.map_inf {α : Type u}