Documentation

Mathlib.Order.Filter.Ultrafilter

Ultrafilters #

An ultrafilter is a minimal (maximal in the set order) proper filter. In this file we define

instance instIsAtomicFilter {α : Type u} :

Filter α is an atomic type: for every filter there exists an ultrafilter that is less than or equal to this filter.

Equations
  • =
structure Ultrafilter (α : Type u_2) extends Filter :
Type u_2

An ultrafilter is a minimal (maximal in the set order) proper filter.

  • sets : Set (Set α)
  • univ_sets : Set.univ (↑self).sets
  • sets_of_superset : ∀ {x y : Set α}, x (↑self).setsx yy (↑self).sets
  • inter_sets : ∀ {x y : Set α}, x (↑self).setsy (↑self).setsx y (↑self).sets
  • neBot' : (↑self).NeBot

    An ultrafilter is nontrivial.

  • le_of_le : ∀ (g : Filter α), g.NeBotg selfself g

    If g is a nontrivial filter that is less than or equal to an ultrafilter, then it is greater than or equal to the ultrafilter.

Instances For
    theorem Ultrafilter.neBot' {α : Type u_2} (self : Ultrafilter α) :
    (↑self).NeBot

    An ultrafilter is nontrivial.

    theorem Ultrafilter.le_of_le {α : Type u_2} (self : Ultrafilter α) (g : Filter α) :
    g.NeBotg selfself g

    If g is a nontrivial filter that is less than or equal to an ultrafilter, then it is greater than or equal to the ultrafilter.

    Equations
    • Ultrafilter.instCoeTCFilter = { coe := Ultrafilter.toFilter }
    Equations
    • Ultrafilter.instMembershipSet = { mem := fun (f : Ultrafilter α) (s : Set α) => s f }
    theorem Ultrafilter.unique {α : Type u} (f : Ultrafilter α) {g : Filter α} (h : g f) (hne : autoParam g.NeBot _auto✝) :
    g = f
    instance Ultrafilter.neBot {α : Type u} (f : Ultrafilter α) :
    (↑f).NeBot
    Equations
    • =
    theorem Ultrafilter.isAtom {α : Type u} (f : Ultrafilter α) :
    IsAtom f
    @[simp]
    theorem Ultrafilter.mem_coe {α : Type u} {f : Ultrafilter α} {s : Set α} :
    s f s f
    theorem Ultrafilter.coe_injective {α : Type u} :
    Function.Injective Ultrafilter.toFilter
    theorem Ultrafilter.eq_of_le {α : Type u} {f : Ultrafilter α} {g : Ultrafilter α} (h : f g) :
    f = g
    @[simp]
    theorem Ultrafilter.coe_le_coe {α : Type u} {f : Ultrafilter α} {g : Ultrafilter α} :
    f g f = g
    @[simp]
    theorem Ultrafilter.coe_inj {α : Type u} {f : Ultrafilter α} {g : Ultrafilter α} :
    f = g f = g
    theorem Ultrafilter.ext_iff {α : Type u} {f : Ultrafilter α} {g : Ultrafilter α} :
    f = g ∀ (s : Set α), s f s g
    theorem Ultrafilter.ext {α : Type u} ⦃f : Ultrafilter α ⦃g : Ultrafilter α (h : ∀ (s : Set α), s f s g) :
    f = g
    theorem Ultrafilter.le_of_inf_neBot {α : Type u} (f : Ultrafilter α) {g : Filter α} (hg : (f g).NeBot) :
    f g
    theorem Ultrafilter.le_of_inf_neBot' {α : Type u} (f : Ultrafilter α) {g : Filter α} (hg : (g f).NeBot) :
    f g
    theorem Ultrafilter.inf_neBot_iff {α : Type u} {f : Ultrafilter α} {g : Filter α} :
    (f g).NeBot f g
    theorem Ultrafilter.disjoint_iff_not_le {α : Type u} {f : Ultrafilter α} {g : Filter α} :
    Disjoint (↑f) g ¬f g
    @[simp]
    theorem Ultrafilter.compl_not_mem_iff {α : Type u} {f : Ultrafilter α} {s : Set α} :
    sf s f
    @[simp]
    theorem Ultrafilter.frequently_iff_eventually {α : Type u} {f : Ultrafilter α} {p : αProp} :
    (∃ᶠ (x : α) in f, p x) ∀ᶠ (x : α) in f, p x
    theorem Filter.Frequently.eventually {α : Type u} {f : Ultrafilter α} {p : αProp} :
    (∃ᶠ (x : α) in f, p x)∀ᶠ (x : α) in f, p x

    Alias of the forward direction of Ultrafilter.frequently_iff_eventually.

    theorem Ultrafilter.compl_mem_iff_not_mem {α : Type u} {f : Ultrafilter α} {s : Set α} :
    s f sf
    theorem Ultrafilter.diff_mem_iff {α : Type u} {s : Set α} {t : Set α} (f : Ultrafilter α) :
    s \ t f s f tf
    def Ultrafilter.ofComplNotMemIff {α : Type u} (f : Filter α) (h : ∀ (s : Set α), sf s f) :

    If sᶜ ∉ f ↔ s ∈ f, then f is an ultrafilter. The other implication is given by Ultrafilter.compl_not_mem_iff.

    Equations
    Instances For
      def Ultrafilter.ofAtom {α : Type u} (f : Filter α) (hf : IsAtom f) :

      If f : Filter α is an atom, then it is an ultrafilter.

      Equations
      Instances For
        theorem Ultrafilter.nonempty_of_mem {α : Type u} {f : Ultrafilter α} {s : Set α} (hs : s f) :
        s.Nonempty
        theorem Ultrafilter.ne_empty_of_mem {α : Type u} {f : Ultrafilter α} {s : Set α} (hs : s f) :
        @[simp]
        theorem Ultrafilter.empty_not_mem {α : Type u} {f : Ultrafilter α} :
        f
        @[simp]
        theorem Ultrafilter.le_sup_iff {α : Type u} {u : Ultrafilter α} {f : Filter α} {g : Filter α} :
        u f g u f u g
        @[simp]
        theorem Ultrafilter.union_mem_iff {α : Type u} {f : Ultrafilter α} {s : Set α} {t : Set α} :
        s t f s f t f
        theorem Ultrafilter.mem_or_compl_mem {α : Type u} (f : Ultrafilter α) (s : Set α) :
        s f s f
        theorem Ultrafilter.em {α : Type u} (f : Ultrafilter α) (p : αProp) :
        (∀ᶠ (x : α) in f, p x) ∀ᶠ (x : α) in f, ¬p x
        theorem Ultrafilter.eventually_or {α : Type u} {f : Ultrafilter α} {p : αProp} {q : αProp} :
        (∀ᶠ (x : α) in f, p x q x) (∀ᶠ (x : α) in f, p x) ∀ᶠ (x : α) in f, q x
        theorem Ultrafilter.eventually_not {α : Type u} {f : Ultrafilter α} {p : αProp} :
        (∀ᶠ (x : α) in f, ¬p x) ¬∀ᶠ (x : α) in f, p x
        theorem Ultrafilter.eventually_imp {α : Type u} {f : Ultrafilter α} {p : αProp} {q : αProp} :
        (∀ᶠ (x : α) in f, p xq x) (∀ᶠ (x : α) in f, p x)∀ᶠ (x : α) in f, q x
        theorem Ultrafilter.finite_sUnion_mem_iff {α : Type u} {f : Ultrafilter α} {s : Set (Set α)} (hs : s.Finite) :
        ⋃₀ s f ts, t f
        theorem Ultrafilter.finite_biUnion_mem_iff {α : Type u} {β : Type v} {f : Ultrafilter α} {is : Set β} {s : βSet α} (his : is.Finite) :
        iis, s i f iis, s i f
        def Ultrafilter.map {α : Type u} {β : Type v} (m : αβ) (f : Ultrafilter α) :

        Pushforward for ultrafilters.

        Equations
        Instances For
          @[simp]
          theorem Ultrafilter.coe_map {α : Type u} {β : Type v} (m : αβ) (f : Ultrafilter α) :
          (Ultrafilter.map m f) = Filter.map m f
          @[simp]
          theorem Ultrafilter.mem_map {α : Type u} {β : Type v} {m : αβ} {f : Ultrafilter α} {s : Set β} :
          @[simp]
          theorem Ultrafilter.map_id {α : Type u} (f : Ultrafilter α) :
          @[simp]
          theorem Ultrafilter.map_id' {α : Type u} (f : Ultrafilter α) :
          Ultrafilter.map (fun (x : α) => x) f = f
          @[simp]
          theorem Ultrafilter.map_map {α : Type u} {β : Type v} {γ : Type u_1} (f : Ultrafilter α) (m : αβ) (n : βγ) :
          def Ultrafilter.comap {α : Type u} {β : Type v} {m : αβ} (u : Ultrafilter β) (inj : Function.Injective m) (large : Set.range m u) :

          The pullback of an ultrafilter along an injection whose range is large with respect to the given ultrafilter.

          Equations
          • u.comap inj large = { toFilter := Filter.comap m u, neBot' := , le_of_le := }
          Instances For
            @[simp]
            theorem Ultrafilter.mem_comap {α : Type u} {β : Type v} {m : αβ} (u : Ultrafilter β) (inj : Function.Injective m) (large : Set.range m u) {s : Set α} :
            s u.comap inj large m '' s u
            @[simp]
            theorem Ultrafilter.coe_comap {α : Type u} {β : Type v} {m : αβ} (u : Ultrafilter β) (inj : Function.Injective m) (large : Set.range m u) :
            (u.comap inj large) = Filter.comap m u
            @[simp]
            theorem Ultrafilter.comap_id {α : Type u} (f : Ultrafilter α) (h₀ : optParam (Function.Injective id) ) (h₁ : optParam (Set.range id f) ) :
            f.comap h₀ h₁ = f
            @[simp]
            theorem Ultrafilter.comap_comap {α : Type u} {β : Type v} {γ : Type u_1} (f : Ultrafilter γ) {m : αβ} {n : βγ} (inj₀ : Function.Injective n) (large₀ : Set.range n f) (inj₁ : Function.Injective m) (large₁ : Set.range m f.comap inj₀ large₀) (inj₂ : optParam (Function.Injective (n m)) ) (large₂ : optParam (Set.range (n m) f) ) :
            (f.comap inj₀ large₀).comap inj₁ large₁ = f.comap inj₂ large₂

            The principal ultrafilter associated to a point x.

            Equations
            @[simp]
            theorem Ultrafilter.mem_pure {α : Type u} {a : α} {s : Set α} :
            s pure a a s
            @[simp]
            theorem Ultrafilter.coe_pure {α : Type u} (a : α) :
            (pure a) = pure a
            @[simp]
            theorem Ultrafilter.map_pure {α : Type u} {β : Type v} (m : αβ) (a : α) :
            @[simp]
            theorem Ultrafilter.comap_pure {α : Type u} {β : Type v} {m : αβ} (a : α) (inj : Function.Injective m) (large : Set.range m pure (m a)) :
            (pure (m a)).comap inj large = pure a
            Equations
            • Ultrafilter.instInhabited = { default := pure default }
            Equations
            • =
            theorem Ultrafilter.eq_pure_of_finite_mem {α : Type u} {f : Ultrafilter α} {s : Set α} (h : s.Finite) (h' : s f) :
            xs, f = pure x
            theorem Ultrafilter.eq_pure_of_finite {α : Type u} [Finite α] (f : Ultrafilter α) :
            ∃ (a : α), f = pure a
            theorem Ultrafilter.le_cofinite_or_eq_pure {α : Type u} (f : Ultrafilter α) :
            f Filter.cofinite ∃ (a : α), f = pure a
            def Ultrafilter.bind {α : Type u} {β : Type v} (f : Ultrafilter α) (m : αUltrafilter β) :

            Monadic bind for ultrafilters, coming from the one on filters defined in terms of map and join.

            Equations
            Instances For
              Equations
              theorem Ultrafilter.exists_le {α : Type u} (f : Filter α) [h : f.NeBot] :
              ∃ (u : Ultrafilter α), u f

              The ultrafilter lemma: Any proper filter is contained in an ultrafilter.

              theorem Filter.exists_ultrafilter_le {α : Type u} (f : Filter α) [h : f.NeBot] :
              ∃ (u : Ultrafilter α), u f

              Alias of Ultrafilter.exists_le.


              The ultrafilter lemma: Any proper filter is contained in an ultrafilter.

              noncomputable def Ultrafilter.of {α : Type u} (f : Filter α) [f.NeBot] :

              Construct an ultrafilter extending a given filter. The ultrafilter lemma is the assertion that such a filter exists; we use the axiom of choice to pick one.

              Equations
              Instances For
                theorem Ultrafilter.of_le {α : Type u} (f : Filter α) [f.NeBot] :
                theorem Ultrafilter.of_coe {α : Type u} (f : Ultrafilter α) :
                theorem Ultrafilter.exists_ultrafilter_of_finite_inter_nonempty {α : Type u} (S : Set (Set α)) (cond : ∀ (T : Finset (Set α)), T S(⋂₀ T).Nonempty) :
                ∃ (F : Ultrafilter α), S (↑F).sets
                theorem Filter.isAtom_pure {α : Type u} {a : α} :
                theorem Filter.NeBot.le_pure_iff {α : Type u} {f : Filter α} {a : α} (hf : f.NeBot) :
                f pure a f = pure a
                theorem Filter.NeBot.eq_pure_iff {α : Type u} {f : Filter α} (hf : f.NeBot) {x : α} :
                f = pure x {x} f
                theorem Filter.atTop_eq_pure_of_isTop {α : Type u} [LinearOrder α] {x : α} (hx : IsTop x) :
                Filter.atTop = pure x
                theorem Filter.atBot_eq_pure_of_isBot {α : Type u} [LinearOrder α] {x : α} (hx : IsBot x) :
                Filter.atBot = pure x
                @[simp]
                theorem Filter.lt_pure_iff {α : Type u} {f : Filter α} {a : α} :
                f < pure a f =
                theorem Filter.le_pure_iff' {α : Type u} {f : Filter α} {a : α} :
                f pure a f = f = pure a
                @[simp]
                theorem Filter.Iic_pure {α : Type u} (a : α) :
                Set.Iic (pure a) = {, pure a}
                theorem Filter.mem_iff_ultrafilter {α : Type u} {f : Filter α} {s : Set α} :
                s f ∀ (g : Ultrafilter α), g fs g
                theorem Filter.le_iff_ultrafilter {α : Type u} {f₁ : Filter α} {f₂ : Filter α} :
                f₁ f₂ ∀ (g : Ultrafilter α), g f₁g f₂
                theorem Filter.iSup_ultrafilter_le_eq {α : Type u} (f : Filter α) :
                ⨆ (g : Ultrafilter α), ⨆ (_ : g f), g = f

                A filter equals the intersection of all the ultrafilters which contain it.

                theorem Filter.tendsto_iff_ultrafilter {α : Type u} {β : Type v} (f : αβ) (l₁ : Filter α) (l₂ : Filter β) :
                Filter.Tendsto f l₁ l₂ ∀ (g : Ultrafilter α), g l₁Filter.Tendsto f (↑g) l₂

                The tendsto relation can be checked on ultrafilters.

                theorem Filter.exists_ultrafilter_iff {α : Type u} {f : Filter α} :
                (∃ (u : Ultrafilter α), u f) f.NeBot
                theorem Filter.forall_neBot_le_iff {α : Type u} {g : Filter α} {p : Filter αProp} (hp : Monotone p) :
                (∀ (f : Filter α), f.NeBotf gp f) ∀ (f : Ultrafilter α), f gp f
                noncomputable def Filter.hyperfilter (α : Type u) [Infinite α] :

                The ultrafilter extending the cofinite filter.

                Equations
                Instances For
                  theorem Filter.hyperfilter_le_cofinite {α : Type u} [Infinite α] :
                  (Filter.hyperfilter α) Filter.cofinite
                  theorem Filter.nmem_hyperfilter_of_finite {α : Type u} [Infinite α] {s : Set α} (hf : s.Finite) :
                  theorem Set.Finite.nmem_hyperfilter {α : Type u} [Infinite α] {s : Set α} (hf : s.Finite) :

                  Alias of Filter.nmem_hyperfilter_of_finite.

                  theorem Filter.compl_mem_hyperfilter_of_finite {α : Type u} [Infinite α] {s : Set α} (hf : s.Finite) :
                  theorem Filter.mem_hyperfilter_of_finite_compl {α : Type u} [Infinite α] {s : Set α} (hf : s.Finite) :
                  theorem Ultrafilter.comap_inf_principal_neBot_of_image_mem {α : Type u} {β : Type v} {m : αβ} {s : Set α} {g : Ultrafilter β} (h : m '' s g) :
                  noncomputable def Ultrafilter.ofComapInfPrincipal {α : Type u} {β : Type v} {m : αβ} {s : Set α} {g : Ultrafilter β} (h : m '' s g) :

                  Ultrafilter extending the inf of a comapped ultrafilter and a principal ultrafilter.

                  Equations
                  Instances For
                    theorem Ultrafilter.ofComapInfPrincipal_mem {α : Type u} {β : Type v} {m : αβ} {s : Set α} {g : Ultrafilter β} (h : m '' s g) :
                    theorem Ultrafilter.ofComapInfPrincipal_eq_of_map {α : Type u} {β : Type v} {m : αβ} {s : Set α} {g : Ultrafilter β} (h : m '' s g) :
                    theorem Ultrafilter.eq_of_le_pure {X : Type u_2} {α : Filter X} (hα : α.NeBot) {x : X} {y : X} (hx : α pure x) (hy : α pure y) :
                    x = y