Documentation

Mathlib.Order.Filter.Defs

Definitions about filters #

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

Main definitions #

Notations #

Implementation Notes #

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.

References #

structure Filter (α : Type u_1) :
Type u_1

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

  • sets : Set (Set α)

    The set of sets that belong to the filter.

  • univ_sets : Set.univ self.sets

    The set Set.univ belongs to any filter.

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

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

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

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

Instances For
    theorem Filter.univ_sets {α : Type u_1} (self : Filter α) :
    Set.univ self.sets

    The set Set.univ belongs to any filter.

    theorem Filter.sets_of_superset {α : Type u_1} (self : Filter α) {x : Set α} {y : Set α} :
    x self.setsx yy self.sets

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

    theorem Filter.inter_sets {α : Type u_1} (self : Filter α) {x : Set α} {y : Set α} :
    x self.setsy self.setsx y self.sets

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

    theorem Filter.filter_eq {α : Type u_1} {f : Filter α} {g : Filter α} :
    f.sets = g.setsf = g
    instance Filter.instMembership {α : Type u_1} :

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

    Equations
    • Filter.instMembership = { mem := fun (F : Filter α) (U : Set α) => U F.sets }
    theorem Filter.ext_iff {α : Type u_1} {f : Filter α} {g : Filter α} :
    f = g ∀ (s : Set α), s f s g
    theorem Filter.ext {α : Type u_1} {f : Filter α} {g : Filter α} (h : ∀ (s : Set α), s f s g) :
    f = g
    @[simp]
    theorem Filter.mem_mk {α : Type u_1} {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_1} {f : Filter α} {s : Set α} :
    s f.sets s f
    @[simp]
    theorem Filter.univ_mem {α : Type u_1} {f : Filter α} :
    Set.univ f
    theorem Filter.mem_of_superset {α : Type u_1} {f : Filter α} {x : Set α} {y : Set α} (hx : x f) (hxy : x y) :
    y f
    theorem Filter.univ_mem' {α : Type u_1} {f : Filter α} {s : Set α} (h : ∀ (a : α), a s) :
    s f
    theorem Filter.inter_mem {α : Type u_1} {f : Filter α} {s : Set α} {t : Set α} (hs : s f) (ht : t f) :
    s t f
    theorem Filter.mp_mem {α : Type u_1} {f : Filter α} {s : Set α} {t : Set α} (hs : s f) (h : {x : α | x sx t} f) :
    t f
    def Filter.copy {α : Type u_1} (f : Filter α) (S : Set (Set α)) (hmem : ∀ (s : Set α), s S s f) :

    Override sets field of a filter to provide better definitional equality.

    Equations
    • f.copy S hmem = { sets := S, univ_sets := , sets_of_superset := , inter_sets := }
    Instances For
      @[simp]
      theorem Filter.mem_copy {α : Type u_1} {f : Filter α} {s : Set α} {S : Set (Set α)} {hmem : ∀ (s : Set α), s S s f} :
      s f.copy S hmem s S
      def Filter.comk {α : Type u_1} (p : Set αProp) (he : p ) (hmono : ∀ (t : Set α), p tst, p s) (hunion : ∀ (s : Set α), p s∀ (t : Set α), p tp (s t)) :

      Construct a filter from a property that is stable under finite unions. A set s belongs to Filter.comk p _ _ _ iff its complement satisfies the predicate p. This constructor is useful to define filters like Filter.cofinite.

      Equations
      • Filter.comk p he hmono hunion = { sets := {t : Set α | p t}, univ_sets := , sets_of_superset := , inter_sets := }
      Instances For
        @[simp]
        theorem Filter.mem_comk {α : Type u_1} {p : Set αProp} {he : p } {hmono : ∀ (t : Set α), p tst, p s} {hunion : ∀ (s : Set α), p s∀ (t : Set α), p tp (s t)} {s : Set α} :
        s Filter.comk p he hmono hunion p s
        def Filter.principal {α : Type u_1} (s : Set α) :

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

        Equations
        • Filter.principal s = { sets := {t : Set α | s t}, univ_sets := , sets_of_superset := , inter_sets := }
        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_1} {s : Set α} {t : Set α} :

            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
            @[simp]
            theorem Filter.mem_pure {α : Type u_1} {a : α} {s : Set α} :
            s pure a a s
            def Filter.ker {α : Type u_1} (f : Filter α) :
            Set α

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

            Equations
            Instances For
              def Filter.join {α : Type u_1} (f : Filter (Filter α)) :

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

              Equations
              • f.join = { sets := {s : Set α | {t : Filter α | s t} f}, univ_sets := , sets_of_superset := , inter_sets := }
              Instances For
                @[simp]
                theorem Filter.mem_join {α : Type u_1} {s : Set α} {f : Filter (Filter α)} :
                s f.join {t : Filter α | s t} f
                Equations
                theorem Filter.le_def {α : Type u_1} {f : Filter α} {g : Filter α} :
                f g xg, x f
                instance Filter.instSupSet {α : Type u_1} :
                Equations
                @[simp]
                theorem Filter.mem_sSup {α : Type u_1} {s : Set α} {S : Set (Filter α)} :
                s sSup S fS, s f
                @[irreducible]
                def Filter.sInf {α : Type u_1} (s : Set (Filter α)) :

                Infimum of a set of filters. This definition is marked as irreducible so that Lean doesn't try to unfold it when unifying expressions.

                Equations
                Instances For
                  instance Filter.instInfSet {α : Type u_1} :
                  Equations
                  • Filter.instInfSet = { sInf := Filter.sInf }
                  theorem Filter.sSup_lowerBounds {α : Type u_1} (s : Set (Filter α)) :
                  instance Filter.instTop {α : Type u_1} :
                  Top (Filter α)
                  Equations
                  theorem Filter.mem_top_iff_forall {α : Type u_1} {s : Set α} :
                  s ∀ (x : α), x s
                  @[simp]
                  theorem Filter.mem_top {α : Type u_1} {s : Set α} :
                  s s = Set.univ
                  instance Filter.instBot {α : Type u_1} :
                  Bot (Filter α)
                  Equations
                  • Filter.instBot = { bot := (sSup ).copy Set.univ }
                  @[simp]
                  theorem Filter.mem_bot {α : Type u_1} {s : Set α} :
                  instance Filter.instInf {α : Type u_1} :
                  Inf (Filter α)

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

                  Equations
                  • Filter.instInf = { inf := fun (f g : Filter α) => { sets := {s : Set α | af, bg, s = a b}, univ_sets := , sets_of_superset := , inter_sets := } }
                  instance Filter.instSup {α : Type u_1} :
                  Sup (Filter α)

                  The supremum of two filters is the filter that contains sets that belong to both filters.

                  Equations
                  class Filter.NeBot {α : Type u_1} (f : Filter α) :

                  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.

                  • ne' : f

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

                  Instances
                    theorem Filter.NeBot.ne' {α : Type u_1} {f : Filter α} [self : f.NeBot] :

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

                    theorem Filter.neBot_iff {α : Type u_1} {f : Filter α} :
                    f.NeBot f
                    def Filter.Eventually {α : Type u_1} (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

                      Pretty printer defined by notation3 command.

                      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
                          def Filter.Frequently {α : Type u_1} (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

                              Pretty printer defined by notation3 command.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                def Filter.EventuallyEq {α : Type u_1} {β : Type u_2} (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
                                    def Filter.EventuallyLE {α : Type u_1} {β : Type u_2} [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
                                        def Filter.map {α : Type u_1} {β : Type u_2} (m : αβ) (f : Filter α) :

                                        The forward map of a filter

                                        Equations
                                        Instances For
                                          def Filter.Tendsto {α : Type u_1} {β : Type u_2} (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
                                            def Filter.comap {α : Type u_1} {β : Type u_2} (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
                                            • Filter.comap m f = { sets := {s : Set α | tf, m ⁻¹' t s}, univ_sets := , sets_of_superset := , inter_sets := }
                                            Instances For
                                              def Filter.prod {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β) :
                                              Filter (α × β)

                                              Product of filters. This is the filter generated by cartesian products of elements of the component filters.

                                              Equations
                                              Instances For
                                                def Filter.coprod {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β) :
                                                Filter (α × β)

                                                Coproduct of filters.

                                                Equations
                                                Instances For
                                                  instance Filter.instSProd {α : Type u_1} {β : Type u_2} :
                                                  SProd (Filter α) (Filter β) (Filter (α × β))
                                                  Equations
                                                  • Filter.instSProd = { sprod := Filter.prod }
                                                  theorem Filter.prod_eq_inf {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β) :
                                                  f ×ˢ g = Filter.comap Prod.fst f Filter.comap Prod.snd g
                                                  def Filter.bind {α : Type u_1} {β : Type u_2} (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_1} {β : Type u_2} (f : Filter (αβ)) (g : Filter α) :

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

                                                    Equations
                                                    • f.seq g = { sets := {s : Set β | uf, tg, mu, xt, m x s}, univ_sets := , sets_of_superset := , inter_sets := }
                                                    Instances For
                                                      def Filter.curry {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β) :
                                                      Filter (α × β)

                                                      This filter is characterized by Filter.eventually_curry_iff: (∀ᶠ (x : α × β) in f.curry g, p x) ↔ ∀ᶠ (x : α) in f, ∀ᶠ (y : β) in g, p (x, y). Useful in adding quantifiers to the middle of Tendstos. See hasFDerivAt_of_tendstoUniformlyOnFilter.

                                                      Equations
                                                      • f.curry g = f.bind fun (a : α) => Filter.map (fun (x : β) => (a, x)) g
                                                      Instances For
                                                        Equations
                                                        def Filter.lift {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Set αFilter β) :

                                                        A variant on bind using a function g taking a set instead of a member of α. This is essentially a push-forward along a function mapping each set to a filter.

                                                        Equations
                                                        • f.lift g = sf, g s
                                                        Instances For
                                                          def Filter.lift' {α : Type u_1} {β : Type u_2} (f : Filter α) (h : Set αSet β) :

                                                          Specialize lift to functions Set α → Set β. This can be viewed as a generalization of map. This is essentially a push-forward along a function mapping each set to a set.

                                                          Equations
                                                          • f.lift' h = f.lift (Filter.principal h)
                                                          Instances For

                                                            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