Documentation

Mathlib.Order.Filter.Basic

Theory of filters on sets #

Main definitions #

Filters on a type X are sets of sets of X satisfying three conditions. They are mostly used to abstract two related kinds of ideas:

In this file, we define the type Filter X of filters on X, and endow 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.

structure Filter (α : Type u_1) :
Type u_1
  • sets : Set (Set α)

    The set of sets that belong to the filter.

  • univ_sets : Set.univ s.sets

    The set Set.univ belongs to any filter.

  • sets_of_superset : ∀ {x y : Set α}, x s.setsx yy s.sets

    If a set belongs to a filter, then its superset belongs to the filter as well.

  • inter_sets : ∀ {x y : Set α}, x s.setsy s.setsx y s.sets

    If two sets belong to a filter, then their intersection belongs to the filter as well.

A filter F on a type α is a collection of sets of α which contains the whole α, is upwards-closed, and is stable under intersection. We do not forbid this collection to be all sets of α.

Instances For
    instance instMembershipSetFilter {α : Type u_1} :

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

    Equations
    • instMembershipSetFilter = { mem := fun U F => U F.sets }
    @[simp]
    theorem Filter.mem_mk {α : Type u} {s : Set α} {t : Set (Set α)} {h₁ : Set.univ t} {h₂ : ∀ {x y : Set α}, x tx yy t} {h₃ : ∀ {x y : Set α}, x ty tx y t} :
    s { sets := t, univ_sets := h₁, sets_of_superset := h₂, inter_sets := h₃ } s t
    @[simp]
    theorem Filter.mem_sets {α : Type u} {f : Filter α} {s : Set α} :
    s f.sets s f
    instance Filter.inhabitedMem {α : Type u} {f : Filter α} :
    Inhabited { s // s f }
    Equations
    • Filter.inhabitedMem = { default := { val := Set.univ, property := (_ : Set.univ f.sets) } }
    theorem Filter.filter_eq {α : Type u} {f : Filter α} {g : Filter α} :
    f.sets = g.setsf = g
    theorem Filter.filter_eq_iff {α : Type u} {f : Filter α} {g : Filter α} :
    f = g f.sets = g.sets
    theorem Filter.ext_iff {α : Type u} {f : Filter α} {g : Filter α} :
    f = g ∀ (s : Set α), s f s g
    theorem Filter.ext {α : Type u} {f : Filter α} {g : Filter α} :
    (∀ (s : Set α), s f s g) → f = g
    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).

    @[simp]
    theorem Filter.univ_mem {α : Type u} {f : Filter α} :
    Set.univ f
    theorem Filter.mem_of_superset {α : Type u} {f : Filter α} {x : Set α} {y : Set α} (hx : x f) (hxy : x y) :
    y f
    theorem Filter.inter_mem {α : Type u} {f : Filter α} {s : Set α} {t : Set α} (hs : s f) (ht : t f) :
    s t f
    @[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.univ_mem' {α : Type u} {f : Filter α} {s : Set α} (h : ∀ (a : α), a s) :
    s f
    theorem Filter.mp_mem {α : Type u} {f : Filter α} {s : Set α} {t : Set α} (hs : s f) (h : {x | x sx t} f) :
    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
    @[simp]
    theorem Filter.biInter_mem {α : Type u} {f : Filter α} {β : Type v} {s : βSet α} {is : Set β} (hf : Set.Finite is) :
    ⋂ (i : β) (_ : i is), s i f ∀ (i : β), i iss i f
    @[simp]
    theorem Filter.biInter_finset_mem {α : Type u} {f : Filter α} {β : Type v} {s : βSet α} (is : Finset β) :
    ⋂ (i : β) (_ : i is), s i f ∀ (i : β), i iss i f
    theorem Finset.iInter_mem_sets {α : Type u} {f : Filter α} {β : Type v} {s : βSet α} (is : Finset β) :
    ⋂ (i : β) (_ : i is), s i f ∀ (i : β), i iss i f

    Alias of Filter.biInter_finset_mem.

    @[simp]
    theorem Filter.sInter_mem {α : Type u} {f : Filter α} {s : Set (Set α)} (hfin : Set.Finite s) :
    ⋂₀ s f ∀ (U : Set α), U sU 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 α} :
    (t, t f t s) s f
    theorem Filter.monotone_mem {α : Type u} {f : Filter α} :
    Monotone fun s => s f
    theorem Filter.exists_mem_and_iff {α : Type u} {f : Filter α} {P : Set αProp} {Q : Set αProp} (hP : Antitone P) (hQ : Antitone Q) :
    ((u, u f P u) u, u f Q u) u, u f P u Q u
    theorem Filter.forall_in_swap {α : Type u} {f : Filter α} {β : Type u_1} {p : Set αβProp} :
    ((a : Set α) → a f(b : β) → p a b) (b : β) → (a : Set α) → a fp a b

    filter_upwards [h₁, ⋯, hₙ] replaces a goal of the form s ∈ f and terms h₁ : t₁ ∈ f, ⋯, hₙ : tₙ ∈ f with ∀ x, x ∈ t₁ → ⋯ → x ∈ tₙ → x ∈ s. The list is an optional parameter, [] being its default value.

    filter_upwards [h₁, ⋯, hₙ] with a₁ a₂ ⋯ aₖ is a short form for { filter_upwards [h₁, ⋯, hₙ], intros a₁ a₂ ⋯ aₖ }.

    filter_upwards [h₁, ⋯, hₙ] using e is a short form for { filter_upwards [h1, ⋯, hn], exact e }.

    Combining both shortcuts is done by writing filter_upwards [h₁, ⋯, hₙ] with a₁ a₂ ⋯ aₖ using e. Note that in this case, the aᵢ terms can be used in e.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def Filter.principal {α : Type u} (s : Set α) :

      The principal filter of s is the collection of all supersets of s.

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

        The principal filter of s is the collection of all supersets of s.

        Equations
        Instances For
          @[simp]
          theorem Filter.mem_principal {α : Type u} {s : Set α} {t : Set α} :
          def Filter.join {α : Type u} (f : Filter (Filter α)) :

          The join of a filter of filters is defined by the relation s ∈ join f ↔ {t | s ∈ t} ∈ f.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem Filter.mem_join {α : Type u} {s : Set α} {f : Filter (Filter α)} :
            s Filter.join f {t | s t} f
            Equations
            theorem Filter.le_def {α : Type u} {f : Filter α} {g : Filter α} :
            f g ∀ (x : Set α), x gx f
            theorem Filter.not_le {α : Type u} {f : Filter α} {g : Filter α} :
            ¬f g s, s g ¬s f
            inductive Filter.GenerateSets {α : Type u} (g : Set (Set α)) :
            Set αProp

            generate_sets 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
              • One or more equations did not get rendered due to their size.
              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 α} :
                def Filter.mkOfClosure {α : Type u} (s : Set (Set α)) (hs : (Filter.generate s).sets = s) :

                mk_of_closure 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
                • One or more equations did not get rendered due to their size.
                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
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    instance Filter.instInfFilter {α : Type u} :
                    Inf (Filter α)

                    The infimum of filters is the filter generated by intersections of elements of the two filters.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    theorem Filter.mem_inf_iff {α : Type u} {f : Filter α} {g : Filter α} {s : Set α} :
                    s f g t₁, t₁ f t₂, 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₁, t₁ f t₂, t₂ g t₁ t₂ s
                    instance Filter.instTopFilter {α : Type u} :
                    Top (Filter α)
                    Equations
                    • One or more equations did not get rendered due to their size.
                    theorem Filter.mem_top_iff_forall {α : Type u} {s : Set α} :
                    s ∀ (x : α), x s
                    @[simp]
                    theorem Filter.mem_top {α : Type u} {s : Set α} :
                    s s = Set.univ
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Equations
                    • Filter.instInhabitedFilter = { default := }
                    class Filter.NeBot {α : Type u} (f : Filter α) :
                    • ne' : f

                      The filter is nontrivial: f ≠ ⊥ or equivalently, ∅ ∉ f.

                    A filter is NeBot if it is not equal to , or equivalently the empty set does not belong to the filter. Bourbaki include this assumption in the definition of a filter but we prefer to have a CompleteLattice structure on Filter _, so we use a typeclass argument in lemmas instead.

                    Instances
                      theorem Filter.neBot_iff {α : Type u} {f : Filter α} :
                      theorem Filter.NeBot.ne {α : Type u} {f : Filter α} (hf : Filter.NeBot f) :
                      @[simp]
                      theorem Filter.not_neBot {α : Type u} {f : Filter α} :
                      theorem Filter.NeBot.mono {α : Type u} {f : Filter α} {g : Filter α} (hf : Filter.NeBot f) (hg : f g) :
                      theorem Filter.neBot_of_le {α : Type u} {f : Filter α} {g : Filter α} [hf : Filter.NeBot f] (hg : f g) :
                      @[simp]
                      theorem Filter.sup_neBot {α : Type u} {f : Filter α} {g : Filter α} :
                      theorem Filter.bot_sets_eq {α : Type u} :
                      .sets = Set.univ
                      theorem Filter.eq_or_neBot {α : Type u} (f : Filter α) :

                      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 = ⋂ (f : Filter α) (_ : f s), 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_bot {α : Type u} {s : Set α} :
                      @[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 ∀ (f : Filter α), f sx 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 α} :
                      Filter.NeBot (⨆ (i : ι), f i) i, Filter.NeBot (f i)
                      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 : Set.Finite I) {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.Finite I V, (∀ (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.Finite I V, (∀ (i : ι), V i s i) (∀ (i : ι), ¬i IV i = Set.univ) U = ⋂ (i : ι) (_ : i I), 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, (∀ (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, (∀ (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 α) :
                      theorem Filter.principal_mono {α : Type u} {s : Set α} {t : Set α} :
                      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.principal_univ {α : Type u} :
                      theorem Filter.generate_eq_biInf {α : Type u} (S : Set (Set α)) :
                      Filter.generate S = ⨅ (s : Set α) (_ : s S), Filter.principal s

                      Lattice equations #

                      theorem Filter.empty_mem_iff_bot {α : Type u} {f : Filter α} :
                      theorem Filter.nonempty_of_mem {α : Type u} {f : Filter α} [hf : Filter.NeBot f] {s : Set α} (hs : s f) :
                      theorem Filter.NeBot.nonempty_of_mem {α : Type u} {f : Filter α} (hf : Filter.NeBot f) {s : Set α} (hs : s f) :
                      @[simp]
                      theorem Filter.empty_not_mem {α : Type u} (f : Filter α) [Filter.NeBot f] :
                      theorem Filter.compl_not_mem {α : Type u} {f : Filter α} {s : Set α} [Filter.NeBot f] (h : s f) :
                      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 s, s f t, t g 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 : Filter.NeBot f) (hs : s f) (ht : t f) :
                      theorem Filter.inf_eq_bot_iff {α : Type u} {f : Filter α} {g : Filter α} :
                      f g = U, U f V, V g U V =
                      theorem Pairwise.exists_mem_filter_of_disjoint {α : Type u} {ι : Type u_2} [Finite ι] {l : ιFilter α} (hd : Pairwise (Disjoint on l)) :
                      s, (∀ (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 : Set.PairwiseDisjoint t l) (ht : Set.Finite t) :
                      s, (∀ (i : ι), s i l i) Set.PairwiseDisjoint t s
                      instance Filter.unique {α : Type u} [IsEmpty α] :

                      There is exactly one filter on an empty type.

                      Equations
                      • Filter.unique = { toInhabited := { default := }, uniq := (_ : ∀ (f : Filter α), f = ) }
                      theorem Filter.eq_top_of_neBot {α : Type u} [Subsingleton α] (l : Filter α) [Filter.NeBot l] :
                      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 α} :
                      (∀ (s : Set α), s fSet.Nonempty s) Filter.NeBot f
                      theorem Filter.eq_sInf_of_mem_iff_exists_mem {α : Type u} {S : Set (Filter α)} {l : Filter α} (h : ∀ {s : Set α}, s l f, f S 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 : ι) (x : p i), f i
                      theorem Filter.iInf_sets_eq {α : Type u} {ι : Sort x} {f : ιFilter α} (h : Directed (fun x x_1 => x x_1) 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 x x_1 => x x_1) 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 x x_1 => x x_1) s) (ne : Set.Nonempty s) {t : Set α} :
                      t ⨅ (i : β) (_ : i s), f i i, i s t f i
                      theorem Filter.biInf_sets_eq {α : Type u} {β : Type v} {f : βFilter α} {s : Set β} (h : DirectedOn (f ⁻¹'o fun x x_1 => x x_1) s) (ne : Set.Nonempty s) :
                      (⨅ (i : β) (_ : i s), f i).sets = ⋃ (i : β) (_ : i s), (f i).sets
                      theorem Filter.iInf_sets_eq_finite {α : Type u} {ι : Type u_2} (f : ιFilter α) :
                      (⨅ (i : ι), f i).sets = ⋃ (t : Finset ι), (⨅ (i : ι) (_ : i t), f i).sets
                      theorem Filter.iInf_sets_eq_finite' {α : Type u} {ι : Sort x} (f : ιFilter α) :
                      (⨅ (i : ι), f i).sets = ⋃ (t : Finset (PLift ι)), (⨅ (i : PLift ι) (_ : i t), f i.down).sets
                      theorem Filter.mem_iInf_finite {α : Type u} {ι : Type u_2} {f : ιFilter α} (s : Set α) :
                      s iInf f t, s ⨅ (i : ι) (_ : i t), f i
                      theorem Filter.mem_iInf_finite' {α : Type u} {ι : Sort x} {f : ιFilter α} (s : Set α) :
                      s iInf f t, s ⨅ (i : PLift ι) (_ : i t), f i.down
                      @[simp]
                      theorem Filter.sup_join {α : Type u} {f₁ : Filter (Filter α)} {f₂ : Filter (Filter α)} :
                      Filter.join f₁ Filter.join f₂ = Filter.join (f₁ f₂)
                      @[simp]
                      theorem Filter.iSup_join {α : Type u} {ι : Sort w} {f : ιFilter (Filter α)} :
                      ⨆ (x : ι), Filter.join (f x) = Filter.join (⨆ (x : ι), f x)
                      Equations
                      Equations
                      • One or more equations did not get rendered due to their size.
                      theorem Filter.mem_iInf_finset {α : Type u} {β : Type v} {s : Finset α} {f : αFilter β} {t : Set β} :
                      t ⨅ (a : α) (_ : a s), f a p, (∀ (a : α), a sp a f a) t = ⋂ (a : α) (_ : a s), p a
                      theorem Filter.iInf_neBot_of_directed' {α : Type u} {ι : Sort x} {f : ιFilter α} [Nonempty ι] (hd : Directed (fun x x_1 => x x_1) f) :
                      (∀ (i : ι), Filter.NeBot (f i)) → Filter.NeBot (iInf f)

                      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 x x_1 => x x_1) f) (hb : ∀ (i : ι), Filter.NeBot (f i)) :

                      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 : Set.Nonempty s) (hd : DirectedOn (fun x x_1 => x x_1) s) (hbot : ¬ s) :
                      theorem Filter.sInf_neBot_of_directed {α : Type u} [Nonempty α] {s : Set (Filter α)} (hd : DirectedOn (fun x x_1 => x x_1) s) (hbot : ¬ s) :
                      theorem Filter.iInf_neBot_iff_of_directed' {α : Type u} {ι : Sort x} {f : ιFilter α} [Nonempty ι] (hd : Directed (fun x x_1 => x x_1) f) :
                      Filter.NeBot (iInf f) ∀ (i : ι), Filter.NeBot (f i)
                      theorem Filter.iInf_neBot_iff_of_directed {α : Type u} {ι : Sort x} {f : ιFilter α} [Nonempty α] (hd : Directed (fun x x_1 => x x_1) f) :
                      Filter.NeBot (iInf f) ∀ (i : ι), Filter.NeBot (f i)
                      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]

                      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 ∀ (V : Set α), V fs V
                      @[simp]
                      theorem Filter.iInf_principal_finset {α : Type u} {ι : Type w} (s : Finset ι) (f : ιSet α) :
                      ⨅ (i : ι) (_ : i s), Filter.principal (f i) = Filter.principal (⋂ (i : ι) (_ : i s), f i)
                      @[simp]
                      theorem Filter.iInf_principal {α : Type u} {ι : Type w} [Finite ι] (f : ιSet α) :
                      ⨅ (i : ι), Filter.principal (f i) = Filter.principal (⋂ (i : ι), f i)
                      theorem Filter.iInf_principal_finite {α : Type u} {ι : Type w} {s : Set ι} (hs : Set.Finite s) (f : ιSet α) :
                      ⨅ (i : ι) (_ : i s), Filter.principal (f i) = Filter.principal (⋂ (i : ι) (_ : i s), f i)
                      theorem Filter.join_mono {α : Type u} {f₁ : Filter (Filter α)} {f₂ : Filter (Filter α)} (h : f₁ f₂) :

                      Eventually #

                      def Filter.Eventually {α : Type u} (p : αProp) (f : Filter α) :

                      f.Eventually p or ∀ᶠ x in f, p x mean that {x | p x} ∈ f. E.g., ∀ᶠ x in atTop, p x means that p holds true for sufficiently large x.

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

                          f.Eventually p or ∀ᶠ x in f, p x mean that {x | p x} ∈ f. E.g., ∀ᶠ x in atTop, p x means that p holds true for sufficiently large x.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            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 : (x : α) → x UP 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
                            @[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 : Filter.NeBot f] {p : Prop} :
                            (∀ᶠ (x : α) in f, p) p
                            theorem Filter.eventually_iff_exists_mem {α : Type u} {p : αProp} {f : Filter α} :
                            (∀ᶠ (x : α) in f, p x) v, v f ((y : α) → y vp y)
                            theorem Filter.Eventually.exists_mem {α : Type u} {p : αProp} {f : Filter α} (hp : ∀ᶠ (x : α) in f, p x) :
                            v, v f ((y : α) → y vp 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} {ι : Type 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 : Set.Finite I) {l : Filter α} {p : ιαProp} :
                            (∀ᶠ (x : α) in l, (i : ι) → i Ip i x) ∀ (i : ι), i I∀ᶠ (x : α) in l, p i x
                            theorem Set.Finite.eventually_all {α : Type u} {ι : Type u_2} {I : Set ι} (hI : Set.Finite I) {l : Filter α} {p : ιαProp} :
                            (∀ᶠ (x : α) in l, (i : ι) → i Ip i x) ∀ (i : ι), i I∀ᶠ (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, (i : ι) → i Ip i x) ∀ (i : ι), i I∀ᶠ (x : α) in l, p i x
                            theorem Finset.eventually_all {α : Type u} {ι : Type u_2} (I : Finset ι) {l : Filter α} {p : ιαProp} :
                            (∀ᶠ (x : α) in l, (i : ι) → i Ip i x) ∀ (i : ι), i I∀ᶠ (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
                            @[simp]
                            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) ∀ (f : Filter α), f fs∀ᶠ (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) (x : α) → x ap x
                            theorem Filter.eventually_inf {α : Type u} {f : Filter α} {g : Filter α} {p : αProp} :
                            (∀ᶠ (x : α) in f g, p x) s, s f t, t g ((x : α) → x s tp 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 #

                            def Filter.Frequently {α : Type u} (p : αProp) (f : Filter α) :

                            f.Frequently p or ∃ᶠ x in f, p x mean that {x | ¬p x} ∉ f. E.g., ∃ᶠ x in atTop, p x means that there exist arbitrarily large x for which p holds true.

                            Equations
                            Instances For

                              f.Frequently p or ∃ᶠ x in f, p x mean that {x | ¬p x} ∉ f. E.g., ∃ᶠ x in atTop, p x means that there exist arbitrarily large x for which p holds true.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  theorem Filter.Eventually.frequently {α : Type u} {f : Filter α} [Filter.NeBot f] {p : αProp} (h : ∀ᶠ (x : α) in f, p x) :
                                  ∃ᶠ (x : α) in f, p x
                                  theorem Filter.frequently_of_forall {α : Type u} {f : Filter α} [Filter.NeBot f] {p : αProp} (h : (x : α) → p x) :
                                  ∃ᶠ (x : α) in f, p x
                                  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 α} [Filter.NeBot f] (hp : ∀ᶠ (x : α) in f, p x) :
                                  x, p x
                                  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 fx, x U 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) Filter.NeBot f
                                  @[simp]
                                  theorem Filter.frequently_false {α : Type u} (f : Filter α) :
                                  ¬∃ᶠ (x : α) in f, False
                                  @[simp]
                                  theorem Filter.frequently_const {α : Type u} {f : Filter α} [Filter.NeBot f] {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 α} [Filter.NeBot f] {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 α} [Filter.NeBot f] {p : αProp} {q : Prop} :
                                  (∃ᶠ (x : α) in f, p x q) (∃ᶠ (x : α) in f, p x) q
                                  @[simp]
                                  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 α} [Filter.NeBot f] {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 α} [Filter.NeBot f] {p : αProp} {q : Prop} :
                                  (∃ᶠ (x : α) in f, p xq) (∀ᶠ (x : α) in f, p x) → q
                                  @[simp]
                                  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) x, x a p x
                                  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) f, f fs ∃ᶠ (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 α} [Filter.NeBot l] (h : ∀ᶠ (x : α) in l, y, r x y) :
                                  f, ∀ᶠ (x : α) in l, r x (f x)

                                  Relation “eventually equal” #

                                  def Filter.EventuallyEq {α : Type u} {β : Type v} (l : Filter α) (f : αβ) (g : αβ) :

                                  Two functions f and g are eventually equal along a filter l if the set of x such that f x = g x belongs to l.

                                  Equations
                                  • (f =ᶠ[l] g) = ∀ᶠ (x : α) in l, f x = g x
                                  Instances For

                                    Two functions f and g are eventually equal along a filter l if the set of x such that f x = g x belongs to l.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      theorem Filter.EventuallyEq.eventually {α : Type u} {β : Type v} {l : Filter α} {f : αβ} {g : αβ} (h : f =ᶠ[l] g) :
                                      ∀ᶠ (x : α) in l, f x = g x
                                      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) :
                                      s, s l 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 s, s l 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
                                      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.symm {α : Type u} {β : Type v} {f : αβ} {g : αβ} {l : Filter α} (H : 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
                                      instance Filter.instTransForAllEventuallyEq {α : Type u} {β : Type v} {l : Filter α} :
                                      Trans (fun x x_1 => x =ᶠ[l] x_1) (fun x x_1 => x =ᶠ[l] x_1) fun x x_1 => x =ᶠ[l] x_1
                                      Equations
                                      • Filter.instTransForAllEventuallyEq = { trans := (_ : ∀ {a b c : αβ}, a =ᶠ[l] bb =ᶠ[l] ca =ᶠ[l] c) }
                                      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.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 𝕜 β] {l : Filter α} {f : αβ} {g : αβ} (h : f =ᶠ[l] g) (c : 𝕜) :
                                      (fun x => c +ᵥ f x) =ᶠ[l] fun x => c +ᵥ g x
                                      theorem Filter.EventuallyEq.const_smul {α : Type u} {β : Type v} {𝕜 : Type u_2} [SMul 𝕜 β] {l : Filter α} {f : αβ} {g : αβ} (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_empty {α : Type u} {s : Set α} {l : Filter α} :
                                      s =ᶠ[l] ∀ᶠ (x : α) in l, ¬x s
                                      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
                                      def Filter.EventuallyLE {α : Type u} {β : Type v} [LE β] (l : Filter α) (f : αβ) (g : αβ) :

                                      A function f is eventually less than or equal to a function g at a filter l.

                                      Equations
                                      Instances For

                                        A function f is eventually less than or equal to a function g at a filter l.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          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.instTransForAllEventuallyLEToLE {α : Type u} {β : Type v} [Preorder β] {l : Filter α} :
                                          Trans (fun x x_1 => x ≤ᶠ[l] x_1) (fun x x_1 => x ≤ᶠ[l] x_1) fun x x_1 => x ≤ᶠ[l] x_1
                                          Equations
                                          • Filter.instTransForAllEventuallyLEToLE = { trans := (_ : ∀ {a b c : αβ}, a ≤ᶠ[l] bb ≤ᶠ[l] ca ≤ᶠ[l] c) }
                                          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.instTransForAllEventuallyEqEventuallyLEToLE {α : Type u} {β : Type v} [Preorder β] {l : Filter α} :
                                          Trans (fun x x_1 => x =ᶠ[l] x_1) (fun x x_1 => x ≤ᶠ[l] x_1) fun x x_1 => x ≤ᶠ[l] x_1
                                          Equations
                                          • Filter.instTransForAllEventuallyEqEventuallyLEToLE = { trans := (_ : ∀ {a b c : αβ}, a =ᶠ[l] bb ≤ᶠ[l] ca ≤ᶠ[l] c) }
                                          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.instTransForAllEventuallyLEToLEEventuallyEq {α : Type u} {β : Type v} [Preorder β] {l : Filter α} :
                                          Trans (fun x x_1 => x ≤ᶠ[l] x_1) (fun x x_1 => x =ᶠ[l] x_1) fun x x_1 => x ≤ᶠ[l] x_1
                                          Equations
                                          • Filter.instTransForAllEventuallyLEToLEEventuallyEq = { trans := (_ : ∀ {a b c : αβ}, a ≤ᶠ[l] bb =ᶠ[l] ca ≤ᶠ[l] c) }
                                          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.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.mul_le_mul {α : Type u} {β : Type v} [MulZeroClass β] [PartialOrder β] [PosMulMono β] [MulPosMono β] {l : Filter α} {f₁ : αβ} {f₂ : αβ} {g₁ : αβ} {g₂ : αβ} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) (hg₀ : 0 ≤ᶠ[l] g₁) (hf₀ : 0 ≤ᶠ[l] f₂) :
                                          f₁ * g₁ ≤ᶠ[l] f₂ * g₂
                                          theorem Filter.EventuallyLE.add_le_add {α : Type u} {β : Type v} [Add β] [Preorder β] [CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x x_1] [CovariantClass β β (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {l : Filter α} {f₁ : αβ} {f₂ : αβ} {g₁ : αβ} {g₂ : αβ} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) :
                                          f₁ + g₁ ≤ᶠ[l] f₂ + g₂
                                          theorem Filter.EventuallyLE.mul_le_mul' {α : Type u} {β : Type v} [Mul β] [Preorder β] [CovariantClass β β (fun x x_1 => x * x_1) fun x x_1 => x x_1] [CovariantClass β β (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {l : Filter α} {f₁ : αβ} {f₂ : αβ} {g₁ : αβ} {g₂ : αβ} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) :
                                          f₁ * g₁ ≤ᶠ[l] f₂ * g₂
                                          theorem Filter.EventuallyLE.mul_nonneg {α : Type u} {β : Type v} [OrderedSemiring β] {l : Filter α} {f : αβ} {g : αβ} (hf : 0 ≤ᶠ[l] f) (hg : 0 ≤ᶠ[l] g) :
                                          0 ≤ᶠ[l] f * g
                                          theorem Filter.eventually_sub_nonneg {α : Type u} {β : Type v} [OrderedRing β] {l : Filter α} {f : αβ} {g : αβ} :
                                          0 ≤ᶠ[l] g - f f ≤ᶠ[l] g
                                          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) :

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

                                          def Filter.map {α : Type u} {β : Type v} (m : αβ) (f : Filter α) :

                                          The forward map of a filter

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            @[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 s, s f 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.

                                            def Filter.comap {α : Type u} {β : Type v} (m : αβ) (f : Filter β) :

                                            The inverse map of a filter. A set s belongs to Filter.comap m f if either of the following equivalent conditions hold.

                                            1. There exists a set t ∈ f such that m ⁻¹' t ⊆ s. This is used as a definition.
                                            2. The set kernImage m s = {y | ∀ x, m x = y → x ∈ s} belongs to f, see Filter.mem_comap'.
                                            3. The set (m '' sᶜ)ᶜ belongs to f, see Filter.mem_comap_iff_compl and Filter.compl_mem_comap.
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              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.fst = xp.snd 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
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                theorem Filter.mem_kernMap {α : Type u} {β : Type v} {m : αβ} {f : Filter α} {s : Set β} :
                                                s Filter.kernMap m f t, t f 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, 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, t f m '' t = s
                                                def Filter.bind {α : Type u} {β : Type v} (f : Filter α) (m : αFilter β) :

                                                The monadic bind operation on filter is defined the usual way in terms of map and join.

                                                Unfortunately, this bind does not result in the expected applicative. See Filter.seq for the applicative instance.

                                                Equations
                                                Instances For
                                                  def Filter.seq {α : Type u} {β : Type v} (f : Filter (αβ)) (g : Filter α) :

                                                  The applicative sequentiation operation. This is not induced by the bind operation.

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

                                                    pure x is the set of sets that contain x. It is equal to 𝓟 {x} but with this definition we have s ∈ pure a defeq a ∈ s.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Equations
                                                    theorem Filter.pure_sets {α : Type u} (a : α) :
                                                    (pure a).sets = {s | 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)
                                                    @[simp]
                                                    theorem Filter.join_pure {α : Type u} (f : Filter α) :
                                                    @[simp]
                                                    theorem Filter.pure_bind {α : Type u} {β : Type v} (a : α) (m : αFilter β) :
                                                    Filter.bind (pure a) m = m a

                                                    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
                                                      @[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 = Filter.bind f m

                                                      map and comap equations #

                                                      @[simp]
                                                      theorem Filter.mem_comap {α : Type u} {β : Type v} {g : Filter β} {m : αβ} {s : Set α} :
                                                      s Filter.comap m g t, t g 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 : ¬x t) :
                                                      Filter.comap (fun x => x) g =
                                                      theorem Filter.comap_const_of_mem {α : Type u} {β : Type v} {g : Filter β} {x : β} (h : ∀ (t : Set β), t gx t) :
                                                      Filter.comap (fun x => x) g =
                                                      theorem Filter.map_const {α : Type u} {β : Type v} {f : Filter α} [Filter.NeBot f] {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) :
                                                      @[simp]
                                                      theorem Filter.comap_principal {α : Type u} {β : Type v} {m : αβ} {t : Set β} :
                                                      @[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 : αβ} :
                                                      @[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.NeBot (Filter.comap m g)) :
                                                      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) = ⨆ (f : Filter β) (_ : f s), 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 => ∀ᶠ (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 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.NeBot (Filter.comap m f) ∀ (t : Set β), t fa, m a t
                                                      theorem Filter.comap_neBot {α : Type u} {β : Type v} {f : Filter β} {m : αβ} (hm : ∀ (t : Set β), t fa, m a t) :
                                                      theorem Filter.comap_neBot_iff_frequently {α : Type u} {β : Type v} {f : Filter β} {m : αβ} :
                                                      Filter.NeBot (Filter.comap m f) ∃ᶠ (y : β) in f, y Set.range m
                                                      theorem Filter.comap_neBot_iff_compl_range {α : Type u} {β : Type v} {f : Filter β} {m : αβ} :
                                                      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 : αβ} :
                                                      @[simp]
                                                      theorem Filter.comap_fst_neBot_iff {α : Type u} {β : Type v} {f : Filter α} :
                                                      theorem Filter.comap_fst_neBot {α : Type u} {β : Type v} [Nonempty β] {f : Filter α} [Filter.NeBot f] :
                                                      @[simp]
                                                      theorem Filter.comap_snd_neBot_iff {α : Type u} {β : Type v} {f : Filter β} :
                                                      theorem Filter.comap_snd_neBot {α : Type u} {β : Type v} [Nonempty α] {f : Filter β} [Filter.NeBot f] :
                                                      theorem Filter.comap_eval_neBot_iff' {ι : Type u_2} {α : ιType u_3} {i : ι} {f : Filter (α i)} :
                                                      @[simp]
                                                      theorem Filter.comap_eval_neBot_iff {ι : Type u_2} {α : ιType u_3} [∀ (j : ι), Nonempty (α j)] {i : ι} {f : Filter (α i)} :
                                                      theorem Filter.comap_eval_neBot {ι : Type u_2} {α : ιType u_3} [∀ (j : ι), Nonempty (α j)] (i : ι) (f : Filter (α i)) [Filter.NeBot f] :
                                                      theorem Filter.comap_inf_principal_neBot_of_image_mem {α : Type u} {β : Type v} {f : Filter β} {m : αβ} (hf : Filter.NeBot f) {s : Set α} (hs : m '' s f) :
                                                      theorem Filter.comap_coe_neBot_of_le_principal {γ : Type w} {s : Set γ} {l : Filter γ} [h : Filter.NeBot l] (h' : l Filter.principal s) :
                                                      Filter.NeBot (Filter.comap Subtype.val l)
                                                      theorem Filter.NeBot.comap_of_surj {α : Type u} {β : Type v} {f : Filter β} {m : αβ} (hf : Filter.NeBot f) (hm : Function.Surjective m) :
                                                      theorem Filter.NeBot.comap_of_image_mem {α : Type u} {β : Type v} {f : Filter β} {m : αβ} (hf : Filter.NeBot f) {s : Set α} (hs : m '' s f) :
                                                      @[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 α} :
                                                      theorem Filter.NeBot.map {α : Type u} {β : Type v} {f : Filter α} (hf : Filter.NeBot f) (m : αβ) :
                                                      theorem Filter.NeBot.of_map {α : Type u} {β : Type v} {f : Filter α} {m : αβ} :
                                                      instance Filter.map_neBot {α : Type u} {β : Type v} {f : Filter α} {m : αβ} [hf : Filter.NeBot f] :
                                                      Equations
                                                      theorem Filter.sInter_comap_sets {α : Type u} {β : Type v} (f : αβ) (F : Filter β) :
                                                      ⋂₀ (Filter.comap f F).sets = ⋂ (U : Set β) (_ : U F), 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 x x_1 => x x_1) 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 x x_1 => x x_1) {x | p x}) (ne : i, p i) :
                                                      Filter.map m (⨅ (i : ι) (x : p i), f i) = ⨅ (i : ι) (x : 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} {β : Type v} {f : Filter α} {g : Filter α} {m : αβ} (h : Function.Injective m) :
                                                      theorem Filter.map_inf' {α : Type u} {β : Type v} {f : Filter α} {g : Filter α} {m : αβ} {t : Set α} (htf : t f) (htg : t g) (h : Set.InjOn m t) :
                                                      theorem Filter.disjoint_map {α : Type u} {β : Type v} {m : αβ} (hm : Function.Injective m) {f₁ : Filter α} {f₂ : Filter α} :
                                                      Disjoint (Filter.map m f₁) (Filter.map m f₂) Disjoint f₁ f₂
                                                      theorem Filter.map_equiv_symm {α : Type u} {β : Type v} (e : α β) (f : Filter β) :
                                                      Filter.map (e.symm) f = Filter.comap (e) f
                                                      theorem Filter.map_eq_comap_of_inverse {α : Type u} {β : Type v} {f : Filter α} {m : αβ} {n : βα} (h₁ : m n = id) (h₂ : n m = id) :
                                                      theorem Filter.comap_equiv_symm {α : Type u} {β : Type v} (e : α β) (f : Filter α) :
                                                      Filter.comap (e.symm) f = Filter.map (e) f
                                                      theorem Filter.map_swap_eq_comap_swap {α : Type u} {β : Type v} {f : Filter (α × β)} :
                                                      Prod.swap <$> f = Filter.comap Prod.swap f
                                                      theorem Filter.map_swap4_eq_comap {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} {f : Filter ((α × β) × γ × δ)} :
                                                      Filter.map (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) f = Filter.comap (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) f

                                                      A useful lemma when dealing with uniformities.

                                                      theorem Filter.le_map {α : Type u} {β : Type v} {f : Filter α} {m : αβ} {g : Filter β} (h : ∀ (s : Set α), s fm '' s g) :
                                                      theorem Filter.le_map_iff {α : Type u} {β : Type v} {f : Filter α} {m : αβ} {g : Filter β} :
                                                      g Filter.map m f ∀ (s : Set α), s fm '' s g
                                                      theorem Filter.push_pull {α : Type u} {β : Type v} (f : αβ) (F : Filter α) (G : Filter β) :
                                                      theorem Filter.push_pull' {α : Type u} {β : Type v} (f : αβ) (F : Filter α) (G : Filter β) :
                                                      theorem Filter.singleton_mem_pure {α : Type u} {a : α} :
                                                      {a} pure a
                                                      @[simp]
                                                      theorem Filter.le_pure_iff {α : Type u} {f : Filter α} {a : α} :
                                                      f pure a {a} f
                                                      theorem Filter.mem_seq_def {α : Type u} {β : Type v} {f : Filter (αβ)} {g : Filter α} {s : Set β} :
                                                      s Filter.seq f g u, u f t, t g ∀ (x : αβ), x u∀ (y : α), y tx y s
                                                      theorem Filter.mem_seq_iff {α : Type u} {β : Type v} {f : Filter (αβ)} {g : Filter α} {s : Set β} :
                                                      s Filter.seq f g u, u f t, t g Set.seq u t s
                                                      theorem Filter.mem_map_seq_iff {α : Type u} {β : Type v} {γ : Type w} {f : Filter α} {g : Filter β} {m : αβγ} {s : Set γ} :
                                                      s Filter.seq (Filter.map m f) g t u, t g u f ∀ (x : α), x u∀ (y : β), y tm x y s
                                                      theorem Filter.seq_mem_seq {α : Type u} {β : Type v} {f : Filter (αβ)} {g : Filter α} {s : Set (αβ)} {t : Set α} (hs : s f) (ht : t g) :
                                                      theorem Filter.le_seq {α : Type u} {β : Type v} {f : Filter (αβ)} {g : Filter α} {h : Filter β} (hh : ∀ (t : Set (αβ)), t f∀ (u : Set α), u gSet.seq t u h) :
                                                      theorem Filter.seq_mono {α : Type u} {β : Type v} {f₁ : Filter (αβ)} {f₂ : Filter (αβ)} {g₁ : Filter α} {g₂ : Filter α} (hf : f₁ f₂) (hg : g₁ g₂) :
                                                      Filter.seq f₁ g₁ Filter.seq f₂ g₂
                                                      @[simp]
                                                      theorem Filter.pure_seq_eq_map {α : Type u} {β : Type v} (g : αβ) (f : Filter α) :
                                                      @[simp]
                                                      theorem Filter.seq_pure {α : Type u} {β : Type v} (f : Filter (αβ)) (a : α) :
                                                      Filter.seq f (pure a) = Filter.map (fun g => g a) f
                                                      @[simp]
                                                      theorem Filter.seq_assoc {α : Type u} {β : Type v} {γ : Type w} (x : Filter α) (g : Filter (αβ)) (h : Filter (βγ)) :
                                                      Filter.seq h (Filter.seq g x) = Filter.seq (Filter.seq (Filter.map (fun x x_1 => x x_1) h) g) x
                                                      theorem Filter.prod_map_seq_comm {α : Type u} {β : Type v} (f : Filter α) (g : Filter β) :
                                                      Filter.seq (Filter.map Prod.mk f) g = Filter.seq (Filter.map (fun b a => (a, b)) g) f
                                                      theorem Filter.seq_eq_filter_seq {α : Type u_2} {β : Type u_2} (f : Filter (αβ)) (g : Filter α) :
                                                      (Seq.seq f fun x => g) = Filter.seq f g

                                                      bind equations #

                                                      @[simp]
                                                      theorem Filter.eventually_bind {α : Type u} {β : Type v} {f : Filter α} {m : αFilter β} {p : βProp} :
                                                      (∀ᶠ (y : β) in Filter.bind f m, p y) ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in m x, p y
                                                      @[simp]
                                                      theorem Filter.eventuallyEq_bind {α : Type u} {β : Type v} {γ : Type w} {f : Filter α} {m : αFilter β} {g₁ : βγ} {g₂ : βγ} :
                                                      g₁ =ᶠ[Filter.bind f m] g₂ ∀ᶠ (x : α) in f, g₁ =ᶠ[m x] g₂
                                                      @[simp]
                                                      theorem Filter.eventuallyLE_bind {α : Type u} {β : Type v} {γ : Type w} [LE γ] {f : Filter α} {m : αFilter β} {g₁ : βγ} {g₂ : βγ} :
                                                      g₁ ≤ᶠ[Filter.bind f m] g₂ ∀ᶠ (x : α) in f, g₁ ≤ᶠ[m x] g₂
                                                      theorem Filter.mem_bind' {α : Type u} {β : Type v} {s : Set β} {f : Filter α} {m : αFilter β} :
                                                      s Filter.bind f m {a | s m a} f
                                                      @[simp]
                                                      theorem Filter.mem_bind {α : Type u} {β : Type v} {s : Set β} {f : Filter α} {m : αFilter β} :
                                                      s Filter.bind f m t, t f ∀ (x : α), x ts m x
                                                      theorem Filter.bind_le {α : Type u} {β : Type v} {f : Filter α} {g : αFilter β} {l : Filter β} (h : ∀ᶠ (x : α) in f, g x l) :
                                                      theorem Filter.bind_mono {α : Type u} {β : Type v} {f₁ : Filter α} {f₂ : Filter α} {g₁ : αFilter β} {g₂ : αFilter β} (hf : f₁ f₂) (hg : g₁ ≤ᶠ[f₁] g₂) :
                                                      Filter.bind f₁ g₁ Filter.bind f₂ g₂
                                                      theorem Filter.bind_inf_principal {α : Type u} {β : Type v} {f : Filter α} {g : αFilter β} {s : Set β} :
                                                      theorem Filter.sup_bind {α : Type u} {β : Type v} {f : Filter α} {g : Filter α} {h : αFilter β} :
                                                      theorem Filter.principal_bind {α : Type u} {β : Type v} {s : Set α} {f : αFilter β} :
                                                      Filter.bind (Filter.principal s) f = ⨆ (x : α) (_ : x s), f x
                                                      theorem Filter.sequence_mono {α : Type u} (as : List (Filter α)) (bs : List (Filter α)) :
                                                      List.Forall₂ (fun x x_1 => x x_1) as bssequence as sequence bs
                                                      theorem Filter.mem_traverse {α' : Type u} {β' : Type u} {γ' : Type u} {f : β'Filter α'} {s : γ'Set α'} (fs : List β') (us : List γ') :
                                                      List.Forall₂ (fun b c => s c f b) fs ustraverse s us traverse f fs
                                                      theorem Filter.mem_traverse_iff {α' : Type u} {β' : Type u} {f : β'Filter α'} (fs : List β') (t : Set (List α')) :
                                                      t traverse f fs us, List.Forall₂ (fun b s => s f b) fs us sequence us t
                                                      def Filter.ker {α : Type u_3} (f : Filter α) :
                                                      Set α

                                                      The kernel of a filter is the intersection of all its sets.

                                                      Equations
                                                      Instances For
                                                        theorem Filter.ker_def {α : Type u_3} (f : Filter α) :
                                                        Filter.ker f = ⋂ (s : Set α) (_ : s f), s
                                                        @[simp]
                                                        theorem Filter.mem_ker {α : Type u_3} {f : Filter α} {a : α} :
                                                        a Filter.ker f ∀ (s : Set α), s fa s
                                                        @[simp]
                                                        theorem Filter.subset_ker {α : Type u_3} {f : Filter α} {s : Set α} :
                                                        s Filter.ker f ∀ (t : Set α), t fs t
                                                        def Filter.gi_principal_ker {α : Type u_3} :
                                                        GaloisCoinsertion Filter.principal Filter.ker

                                                        Filter.principal forms a Galois coinsertion with Filter.ker.

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          theorem Filter.ker_mono {α : Type u_3} :
                                                          Monotone Filter.ker
                                                          @[simp]
                                                          theorem Filter.ker_bot {α : Type u_3} :
                                                          @[simp]
                                                          theorem Filter.ker_top {α : Type u_3} :
                                                          Filter.ker = Set.univ
                                                          @[simp]
                                                          theorem Filter.ker_eq_univ {α : Type u_3} {f : Filter α} :
                                                          Filter.ker f = Set.univ f =
                                                          @[simp]
                                                          theorem Filter.ker_inf {α : Type u_3} (f : Filter α) (g : Filter α) :
                                                          @[simp]
                                                          theorem Filter.ker_iInf {ι : Sort u_2} {α : Type u_3} (f : ιFilter α) :
                                                          Filter.ker (⨅ (i : ι), f i) = ⨅ (i : ι), Filter.ker (f i)
                                                          @[simp]
                                                          theorem Filter.ker_sInf {α : Type u_3} (S : Set (Filter α)) :
                                                          Filter.ker (sInf S) = ⨅ (f : Filter α) (_ : f S), Filter.ker f
                                                          @[simp]
                                                          theorem Filter.ker_principal {α : Type u_3} (s : Set α) :
                                                          @[simp]
                                                          theorem Filter.ker_pure {α : Type u_3} (a : α) :
                                                          Filter.ker (pure a) = {a}
                                                          @[simp]
                                                          theorem Filter.ker_comap {α : Type u_3} {β : Type u_4} (m : αβ) (f : Filter β) :

                                                          Limits #

                                                          def Filter.Tendsto {α : Type u} {β : Type v} (f : αβ) (l₁ : Filter α) (l₂ : Filter β) :

                                                          Filter.Tendsto is the generic "limit of a function" predicate. Tendsto f l₁ l₂ asserts that for every l₂ neighborhood a, the f-preimage of a is an l₁ neighborhood.

                                                          Equations
                                                          Instances For
                                                            theorem Filter.tendsto_def {α : Type u} {β : Type v} {f : αβ} {l₁ : Filter α} {l₂ : Filter β} :
                                                            Filter.Tendsto f l₁ l₂ ∀ (s : Set β), s l₂f ⁻¹' s l₁
                                                            theorem Filter.tendsto_iff_eventually {α : Type u} {β : Type v} {f : αβ} {l₁ : Filter α} {l₂ : Filter β} :
                                                            Filter.Tendsto f l₁ l₂ ∀ ⦃p : βProp⦄, (∀ᶠ (y : β) in l₂, p y) → ∀ᶠ (x : α) in l₁, p (f x)
                                                            theorem Filter.Tendsto.eventually {α : Type u} {β : Type v} {f : αβ} {l₁ : Filter α} {l₂ : Filter β} {p : βProp} (hf : Filter.Tendsto f l₁ l₂) (h : ∀ᶠ (y : β) in l₂, p y) :
                                                            ∀ᶠ (x : α) in l₁, p (f x)
                                                            theorem Filter.Tendsto.frequently {α : Type u} {β : Type v} {f : αβ} {l₁ : Filter α} {l₂ : Filter β} {p : βProp} (hf : Filter.Tendsto f l₁ l₂) (h : ∃ᶠ (x : α) in l₁, p (f x)) :
                                                            ∃ᶠ (y : β) in l₂, p y
                                                            theorem Filter.Tendsto.frequently_map {α : Type u} {β : Type v} {l₁ : Filter α} {l₂ : Filter β} {p : αProp} {q : βProp} (f : αβ) (c : Filter.Tendsto f l₁ l₂) (w : (x : α) → p xq (f x)) (h : ∃ᶠ (x : α) in l₁, p x) :
                                                            ∃ᶠ (y : β) in l₂, q y
                                                            @[simp]
                                                            theorem Filter.tendsto_bot {α : Type u} {β : Type v} {f : αβ} {l : Filter β} :
                                                            @[simp]
                                                            theorem Filter.tendsto_top {α : Type u} {β : Type v} {f : αβ} {l : Filter α} :
                                                            theorem Filter.le_map_of_right_inverse {α : Type u} {β : Type v} {mab : αβ} {mba : βα} {f : Filter α} {g : Filter β} (h₁ : mab mba =ᶠ[g] id) (h₂ : Filter.Tendsto mba g f) :
                                                            g Filter.map mab f
                                                            theorem Filter.tendsto_of_isEmpty {α : Type u} {β : Type v} [IsEmpty α] {f : αβ} {la : Filter α} {lb : Filter β} :
                                                            theorem Filter.eventuallyEq_of_left_inv_of_right_inv {α : Type u} {β : Type v} {f : αβ} {g₁ : βα} {g₂ : βα} {fa : Filter α} {fb : Filter β} (hleft : ∀ᶠ (x : α) in fa, g₁ (f x) = x) (hright : ∀ᶠ (y : β) in fb, f (g₂ y) = y) (htendsto : Filter.Tendsto g₂ fb fa) :
                                                            g₁ =ᶠ[fb] g₂
                                                            theorem Filter.tendsto_iff_comap {α : Type u} {β : Type v} {f : αβ} {l₁ : Filter α} {l₂ : Filter β} :
                                                            Filter.Tendsto f l₁ l₂ l₁ Filter.comap f l₂
                                                            theorem Filter.Tendsto.le_comap {α : Type u} {β : Type v} {f : αβ} {l₁ : Filter α} {l₂ : Filter β} :
                                                            Filter.Tendsto f l₁ l₂l₁ Filter.comap f l₂

                                                            Alias of the forward direction of Filter.tendsto_iff_comap.

                                                            theorem Filter.Tendsto.disjoint {α : Type u} {β : Type v} {f : αβ} {la₁ : Filter α} {la₂ : Filter α} {lb₁ : Filter β} {lb₂ : Filter β} (h₁ : Filter.Tendsto f la₁ lb₁) (hd : Disjoint lb₁ lb₂) (h₂ : Filter.Tendsto f la₂ lb₂) :
                                                            Disjoint la₁ la₂
                                                            theorem Filter.tendsto_congr' {α : Type u} {β : Type v} {f₁ : αβ} {f₂ : αβ} {l₁ : Filter α} {l₂ : Filter β} (hl : f₁ =ᶠ[l₁] f₂) :
                                                            Filter.Tendsto f₁ l₁ l₂ Filter.Tendsto f₂ l₁ l₂
                                                            theorem Filter.Tendsto.congr' {α : Type u} {β : Type v} {f₁ : αβ} {f₂ : αβ} {l₁ : Filter α} {l₂ : Filter β} (hl : f₁ =ᶠ[l₁] f₂) (h : Filter.Tendsto f₁ l₁ l₂) :
                                                            Filter.Tendsto f₂ l₁ l₂
                                                            theorem Filter.tendsto_congr {α : Type u} {β : Type v} {f₁ : αβ} {f₂ : αβ} {l₁ : Filter α} {l₂ : Filter β} (h : ∀ (x : α), f₁ x = f₂ x) :
                                                            Filter.Tendsto f₁ l₁ l₂ Filter.Tendsto f₂ l₁ l₂
                                                            theorem Filter.Tendsto.congr {α : Type u} {β : Type v} {f₁ : αβ} {f₂ : αβ} {l₁ : Filter α} {l₂ : Filter β} (h : ∀ (x : α), f₁ x = f₂ x) :
                                                            Filter.Tendsto f₁ l₁ l₂Filter.Tendsto f₂ l₁ l₂
                                                            theorem Filter.tendsto_id' {α : Type u} {x : Filter α} {y : Filter α} :
                                                            theorem Filter.tendsto_id {α : Type u} {x : Filter α} :
                                                            theorem Filter.Tendsto.comp {α : Type u} {β : Type v} {γ : Type w} {f : αβ} {g : βγ} {x : Filter α} {y : Filter β} {z : Filter γ} (hg : Filter.Tendsto g y z) (hf : Filter.Tendsto f x y) :
                                                            theorem Filter.Tendsto.mono_left {α : Type u} {β : Type v} {f : αβ} {x : Filter α} {y : Filter α} {z : Filter β} (hx : Filter.Tendsto f x z) (h : y x) :
                                                            theorem Filter.Tendsto.mono_right {α : Type u} {β : Type v} {f : αβ} {x : Filter α} {y : Filter β} {z : Filter β} (hy : Filter.Tendsto f x y) (hz : y z) :
                                                            theorem Filter.Tendsto.neBot {α : Type u} {β : Type v} {f : αβ} {x : Filter α} {y : Filter β} (h : Filter.Tendsto f x y) [hx : Filter.NeBot x] :
                                                            theorem Filter.tendsto_map {α : Type u} {β : Type v} {f : αβ} {x : Filter α} :
                                                            @[simp]
                                                            theorem Filter.tendsto_map'_iff {α : Type u} {β : Type v} {γ : Type w} {f : βγ} {g : αβ} {x : Filter α} {y : Filter γ} :
                                                            theorem Filter.tendsto_map' {α : Type u} {β : Type v} {γ : Type w} {f : βγ} {g : αβ} {x : Filter α} {y : Filter γ} :

                                                            Alias of the reverse direction of Filter.tendsto_map'_iff.

                                                            theorem Filter.tendsto_comap {α : Type u} {β : Type v} {f : αβ} {x : Filter β} :
                                                            @[simp]
                                                            theorem Filter.tendsto_comap_iff {α : Type u} {β : Type v} {γ : Type w} {f : αβ} {g : βγ} {a : Filter α} {c : Filter γ} :
                                                            theorem Filter.tendsto_comap'_iff {α : Type u} {β : Type v} {γ : Type w} {m : αβ} {f : Filter α} {g : Filter β} {i : γα} (h : Set.range i f) :
                                                            theorem Filter.Tendsto.of_tendsto_comp {α : Type u} {β : Type v} {γ : Type w} {f : αβ} {g : βγ} {a : Filter α} {b : Filter β} {c : Filter γ} (hfg : Filter.Tendsto (g f) a c) (hg : Filter.comap g c b) :
                                                            theorem Filter.comap_eq_of_inverse {α : Type u} {β : Type v} {f : Filter α} {g : Filter β} {φ : αβ} (ψ : βα) (eq : ψ φ = id) (hφ : Filter.Tendsto φ f g) (hψ : Filter.Tendsto ψ g f) :
                                                            theorem Filter.map_eq_of_inverse {α : Type u} {β : Type v} {f : Filter α} {g : Filter β} {φ : αβ} (ψ : βα) (eq : φ ψ = id) (hφ : Filter.Tendsto φ f g) (hψ : Filter.Tendsto ψ g f) :
                                                            Filter.map φ f = g
                                                            theorem Filter.tendsto_inf {α : Type u} {β : Type v} {f : αβ} {x : Filter α} {y₁ : Filter β} {y₂ : Filter β} :
                                                            Filter.Tendsto f x (y₁ y₂) Filter.Tendsto f x y₁ Filter.Tendsto f x y₂
                                                            theorem Filter.tendsto_inf_left {α : Type u} {β : Type v} {f : αβ} {x₁ : Filter α} {x₂ : Filter α} {y : Filter β} (h : Filter.Tendsto f x₁ y) :
                                                            Filter.Tendsto f (x₁ x₂) y
                                                            theorem Filter.tendsto_inf_right {α : Type u} {β : Type v} {f : αβ} {x₁ : Filter α} {x₂ : Filter α} {y : Filter β} (h : Filter.Tendsto f x₂ y) :
                                                            Filter.Tendsto f (x₁ x₂) y
                                                            theorem Filter.Tendsto.inf {α : Type u} {β : Type v} {f : αβ} {x₁ : Filter α} {x₂ : Filter α} {y₁ : Filter β} {y₂ : Filter β} (h₁ : Filter.Tendsto f x₁ y₁) (h₂ : Filter.Tendsto f x₂ y₂) :
                                                            Filter.Tendsto f (x₁ x₂) (y₁ y₂)
                                                            @[simp]
                                                            theorem Filter.tendsto_iInf {α : Type u} {β : Type v} {ι : Sort x} {f : αβ} {x : Filter α} {y : ιFilter β} :
                                                            Filter.Tendsto f x (⨅ (i : ι), y i) ∀ (i : ι), Filter.Tendsto f x (y i)
                                                            theorem Filter.tendsto_iInf' {α : Type u} {β : Type v} {ι : Sort x} {f : αβ} {x : ιFilter α} {y : Filter β} (i : ι) (hi : Filter.Tendsto f (x i) y) :
                                                            Filter.Tendsto f (⨅ (i : ι), x i) y
                                                            theorem Filter.tendsto_iInf_iInf {α : Type u} {β : Type v} {ι : Sort x} {f : αβ} {x : ιFilter α} {y : ιFilter β} (h : ∀ (i : ι), Filter.Tendsto f (x i) (y i)) :
                                                            @[simp]
                                                            theorem Filter.tendsto_sup {α : Type u} {β : Type v} {f : αβ} {x₁ : Filter α} {x₂ : Filter α} {y : Filter β} :
                                                            Filter.Tendsto f (x₁ x₂) y Filter.Tendsto f x₁ y Filter.Tendsto f x₂ y
                                                            theorem Filter.Tendsto.sup {α : Type u} {β : Type v} {f : αβ} {x₁ : Filter α} {x₂ : Filter α} {y : Filter β} :
                                                            Filter.Tendsto f x₁ yFilter.Tendsto f x₂ yFilter.Tendsto f (x₁ x₂) y
                                                            @[simp]
                                                            theorem Filter.tendsto_iSup {α : Type u} {β : Type v} {ι : Sort x} {f : αβ} {x : ιFilter α} {y : Filter β} :
                                                            Filter.Tendsto f (⨆ (i : ι), x i) y ∀ (i : ι), Filter.Tendsto f (x i) y
                                                            theorem Filter.tendsto_iSup_iSup {α : Type u} {β : Type v} {ι : Sort x} {f : αβ} {x : ιFilter α} {y : ιFilter β} (h : ∀ (i : ι), Filter.Tendsto f (x i) (y i)) :
                                                            @[simp]
                                                            theorem Filter.tendsto_principal {α : Type u} {β : Type v} {f : αβ} {l : Filter α} {s : Set β} :
                                                            Filter.Tendsto f l (Filter.principal s) ∀ᶠ (a : α) in l, f a s
                                                            theorem Filter.tendsto_principal_principal {α : Type u} {β : Type v} {f : αβ} {s : Set α} {t : Set β} :
                                                            Filter.Tendsto f (Filter.principal s) (Filter.principal t) ∀ (a : α), a sf a t
                                                            @[simp]
                                                            theorem Filter.tendsto_pure {α : Type u} {β : Type v} {f : αβ} {a : Filter α} {b : β} :
                                                            Filter.Tendsto f a (pure b) ∀ᶠ (x : α) in a, f x = b
                                                            theorem Filter.tendsto_pure_pure {α : Type u} {β : Type v} (f : αβ) (a : α) :
                                                            Filter.Tendsto f (pure a) (pure (f a))
                                                            theorem Filter.tendsto_const_pure {α : Type u} {β : Type v} {a : Filter α} {b : β} :
                                                            Filter.Tendsto (fun x => b) a (pure b)
                                                            theorem Filter.pure_le_iff {α : Type u} {a : α} {l : Filter α} :
                                                            pure a l ∀ (s : Set α), s la s
                                                            theorem Filter.tendsto_pure_left {α : Type u} {β : Type v} {f : αβ} {a : α} {l : Filter β} :
                                                            Filter.Tendsto f (pure a) l ∀ (s : Set β), s lf a s
                                                            @[simp]
                                                            theorem Filter.map_inf_principal_preimage {α : Type u} {β : Type v} {f : αβ} {s : Set β} {l : Filter α} :
                                                            theorem Filter.Tendsto.not_tendsto {α : Type u} {β : Type v} {f : αβ} {a : Filter α} {b₁ : Filter β} {b₂ : Filter β} (hf : Filter.Tendsto f a b₁) [Filter.NeBot a] (hb : Disjoint b₁ b₂) :

                                                            If two filters are disjoint, then a function cannot tend to both of them along a non-trivial filter.

                                                            theorem Filter.Tendsto.if {α : Type u} {β : Type v} {l₁ : Filter α} {l₂ : Filter β} {f : αβ} {g : αβ} {p : αProp} [(x : α) → Decidable (p x)] (h₀ : Filter.Tendsto f (l₁ Filter.principal {x | p x}) l₂) (h₁ : Filter.Tendsto g (l₁ Filter.principal {x | ¬p x}) l₂) :
                                                            Filter.Tendsto (fun x => if p x then f x else g x) l₁ l₂
                                                            theorem Filter.Tendsto.if' {α : Type u_2} {β : Type u_3} {l₁ : Filter α} {l₂ : Filter β} {f : αβ} {g : αβ} {p : αProp} [DecidablePred p] (hf : Filter.Tendsto f l₁ l₂) (hg : Filter.Tendsto g l₁ l₂) :
                                                            Filter.Tendsto (fun a => if p a then f a else g a) l₁ l₂
                                                            theorem Filter.Tendsto.piecewise {α : Type u} {β : Type v} {l₁ : Filter α} {l₂ : Filter β} {f : αβ} {g : αβ} {s : Set α} [(x : α) → Decidable (x s)] (h₀ : Filter.Tendsto f (l₁ Filter.principal s) l₂) (h₁ : Filter.Tendsto g (l₁ Filter.principal s) l₂) :
                                                            Filter.Tendsto (Set.piecewise s f g) l₁ l₂
                                                            theorem Set.EqOn.eventuallyEq {α : Type u_1} {β : Type u_2} {s : Set α} {f : αβ} {g : αβ} (h : Set.EqOn f g s) :
                                                            theorem Set.EqOn.eventuallyEq_of_mem {α : Type u_1} {β : Type u_2} {s : Set α} {l : Filter α} {f : αβ} {g : αβ} (h : Set.EqOn f g s) (hl : s l) :
                                                            f =ᶠ[l] g
                                                            theorem HasSubset.Subset.eventuallyLE {α : Type u_1} {l : Filter α} {s : Set α} {t : Set α} (h : s t) :
                                                            theorem Set.MapsTo.tendsto {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : αβ} (h : Set.MapsTo f s t) :