Documentation

Mathlib.Order.Filter.Ultrafilter.Defs

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.

structure Ultrafilter (α : Type u_2) extends Filter α :
Type u_2

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

Instances For
    Equations
      Equations
        theorem Ultrafilter.unique {α : Type u} (f : Ultrafilter α) {g : Filter α} (h : g f) (hne : g.NeBot := by infer_instance) :
        g = f
        instance Ultrafilter.neBot {α : Type u} (f : Ultrafilter α) :
        (↑f).NeBot
        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.eq_of_le {α : Type u} {f g : Ultrafilter α} (h : f g) :
        f = g
        @[simp]
        theorem Ultrafilter.coe_le_coe {α : Type u} {f g : Ultrafilter α} :
        f g f = g
        @[simp]
        theorem Ultrafilter.coe_inj {α : Type u} {f g : Ultrafilter α} :
        f = g f = g
        theorem Ultrafilter.ext {α : Type u} f g : Ultrafilter α (h : ∀ (s : Set α), s f s g) :
        f = g
        theorem Ultrafilter.ext_iff {α : Type u} {f g : Ultrafilter α} :
        f = g ∀ (s : Set α), s f s g
        theorem Ultrafilter.le_of_inf_neBot {α : Type u} (f : Ultrafilter α) {g : Filter α} (hg : (fg).NeBot) :
        f g
        theorem Ultrafilter.le_of_inf_neBot' {α : Type u} (f : Ultrafilter α) {g : Filter α} (hg : (gf).NeBot) :
        f g
        theorem Ultrafilter.inf_neBot_iff {α : Type u} {f : Ultrafilter α} {g : Filter α} :
        (fg).NeBot f g
        theorem Ultrafilter.disjoint_iff_not_le {α : Type u} {f : Ultrafilter α} {g : Filter α} :
        Disjoint (↑f) g ¬f g
        @[simp]
        theorem Ultrafilter.compl_notMem_iff {α : Type u} {f : Ultrafilter α} {s : Set α} :
        sf s f
        @[deprecated Ultrafilter.compl_notMem_iff (since := "2025-05-23")]
        theorem Ultrafilter.compl_not_mem_iff {α : Type u} {f : Ultrafilter α} {s : Set α} :
        sf s f

        Alias of Ultrafilter.compl_notMem_iff.

        @[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_notMem {α : Type u} {f : Ultrafilter α} {s : Set α} :
        s f sf
        @[deprecated Ultrafilter.compl_mem_iff_notMem (since := "2025-05-23")]
        theorem Ultrafilter.compl_mem_iff_not_mem {α : Type u} {f : Ultrafilter α} {s : Set α} :
        s f sf

        Alias of Ultrafilter.compl_mem_iff_notMem.

        theorem Ultrafilter.diff_mem_iff {α : Type u} {s 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_notMem_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) :
                theorem Ultrafilter.ne_empty_of_mem {α : Type u} {f : Ultrafilter α} {s : Set α} (hs : s f) :
                @[simp]
                theorem Ultrafilter.empty_notMem {α : Type u} {f : Ultrafilter α} :
                f
                @[deprecated Ultrafilter.empty_notMem (since := "2025-05-23")]
                theorem Ultrafilter.empty_not_mem {α : Type u} {f : Ultrafilter α} :
                f

                Alias of Ultrafilter.empty_notMem.

                @[simp]
                theorem Ultrafilter.le_sup_iff {α : Type u} {u : Ultrafilter α} {f g : Filter α} :
                u fg u f u g
                @[simp]
                theorem Ultrafilter.union_mem_iff {α : Type u} {f : Ultrafilter α} {s 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 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 q : αProp} :
                (∀ᶠ (x : α) in f, p xq x) (∀ᶠ (x : α) in f, p x)∀ᶠ (x : α) in f, q x
                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 α) :
                    (map m f) = Filter.map m f
                    @[simp]
                    theorem Ultrafilter.mem_map {α : Type u} {β : Type v} {m : αβ} {f : Ultrafilter α} {s : Set β} :
                    s map m f m ⁻¹' s f
                    @[simp]
                    theorem Ultrafilter.map_id {α : Type u} (f : Ultrafilter α) :
                    map id f = f
                    @[simp]
                    theorem Ultrafilter.map_id' {α : Type u} (f : Ultrafilter α) :
                    map (fun (x : α) => x) f = f
                    @[simp]
                    theorem Ultrafilter.map_map {α : Type u} {β : Type v} {γ : Type u_1} (f : Ultrafilter α) (m : αβ) (n : βγ) :
                    map n (map m f) = map (n m) f
                    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
                      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₀ : Function.Injective id := ) (h₁ : 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₂ : Function.Injective (n m) := ) (large₂ : 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 : α) :
                          map m (pure a) = pure (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
                          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
                              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] :
                                  (of f) f
                                  theorem Ultrafilter.of_coe {α : Type u} (f : Ultrafilter α) :
                                  of f = f
                                  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
                                  @[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 : α) :
                                  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₁ 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.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
                                  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} ( : α.NeBot) {x y : X} (hx : α pure x) (hy : α pure y) :
                                      x = y