Mathlib.Order.Filter.Ultrafilter.Defs

instIsAtomicFilter instance

: IsAtomic (Filter α)

Full source

/-- `Filter α` is an atomic type: for every filter there exists an ultrafilter that is less than or
equal to this filter. -/
instance : IsAtomic (Filter α) :=
  IsAtomic.of_isChain_bounded fun c hc hne hb =>
    ⟨sInf c, (sInf_neBot_of_directed' hne (show IsChain (· ≥ ·) c from hc.symm).directedOn hb).ne,
      fun _ hx => sInf_le hx⟩

Atomicity of the Filter Lattice

Informal description

The lattice of filters on any type $\alpha$ is atomic, meaning that every proper filter is contained in some ultrafilter.

Ultrafilter structure

(α : Type*) extends Filter α

Full source

/-- An ultrafilter is a minimal (maximal in the set order) proper filter. -/
structure Ultrafilter (α : Type*) extends Filter α where
  /-- An ultrafilter is nontrivial. -/
  protected neBot' : NeBot toFilter
  /-- 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. -/
  protected le_of_le : ∀ g, Filter.NeBot g → g ≤ toFilter → toFilter ≤ g

Ultrafilter

Informal description

An ultrafilter on a type $\alpha$ is a maximal proper filter with respect to the inclusion order. It is a filter that cannot be extended to a larger proper filter.

Ultrafilter.instCoeTCFilter instance

: CoeTC (Ultrafilter α) (Filter α)

Full source

instance : CoeTC (Ultrafilter α) (Filter α) :=
  ⟨Ultrafilter.toFilter⟩

Ultrafilter as Filter

Informal description

Every ultrafilter on a type $\alpha$ can be viewed as a filter on $\alpha$ through a canonical inclusion.

Ultrafilter.instMembershipSet instance

: Membership (Set α) (Ultrafilter α)

Full source

instance : Membership (Set α) (Ultrafilter α) :=
  ⟨fun f s => s ∈ (f : Filter α)⟩

Membership Relation for Sets in Ultrafilters

Informal description

For any set $s$ of type $\alpha$ and any ultrafilter $f$ on $\alpha$, we say $s \in f$ if $s$ is a member of the underlying filter of $f$.

Ultrafilter.neBot instance

(f : Ultrafilter α) : NeBot (f : Filter α)

Full source

instance neBot (f : Ultrafilter α) : NeBot (f : Filter α) :=
  f.neBot'

Ultrafilters are Nontrivial

Informal description

For any ultrafilter $f$ on a type $\alpha$, the underlying filter of $f$ is not the trivial (bottom) filter.

Ultrafilter.isAtom theorem

(f : Ultrafilter α) : IsAtom (f : Filter α)

Full source

protected theorem isAtom (f : Ultrafilter α) : IsAtom (f : Filter α) :=
  ⟨f.neBot.ne, fun _ hgf => by_contra fun hg => hgf.ne <| f.unique hgf.le ⟨hg⟩⟩

Ultrafilters are Atoms in the Filter Lattice

Informal description

For any ultrafilter $f$ on a type $\alpha$, the underlying filter of $f$ is an atom in the lattice of filters on $\alpha$. That is, it is a minimal non-trivial filter with respect to the inclusion order.

Ultrafilter.mem_coe theorem

: s ∈ (f : Filter α) ↔ s ∈ f

Full source

@[simp, norm_cast]
theorem mem_coe : s ∈ (f : Filter α)s ∈ (f : Filter α) ↔ s ∈ f :=
  Iff.rfl

Membership Equivalence for Ultrafilters and Their Underlying Filters

Informal description

For any set $s$ in a type $\alpha$ and any ultrafilter $f$ on $\alpha$, the set $s$ belongs to the underlying filter of $f$ if and only if $s$ belongs to $f$.

Ultrafilter.coe_injective theorem

: Injective ((↑) : Ultrafilter α → Filter α)

Full source

theorem coe_injective : Injective ((↑) : Ultrafilter α → Filter α)
  | ⟨f, h₁, h₂⟩, ⟨g, _, _⟩, _ => by congr

Injectivity of the Ultrafilter Embedding

Informal description

The canonical embedding from the type of ultrafilters on $\alpha$ to the type of filters on $\alpha$ is injective. In other words, if two ultrafilters $f$ and $g$ on $\alpha$ have the same underlying filter, then $f = g$.

Ultrafilter.coe_le_coe theorem

{f g : Ultrafilter α} : (f : Filter α) ≤ g ↔ f = g

Full source

@[simp, norm_cast]
theorem coe_le_coe {f g : Ultrafilter α} : (f : Filter α) ≤ g ↔ f = g :=
  ⟨fun h => eq_of_le h, fun h => h ▸ le_rfl⟩

Ultrafilter Ordering via Underlying Filter: $f \leq g \leftrightarrow f = g$

Informal description

For any two ultrafilters $f$ and $g$ on a type $\alpha$, the underlying filter of $f$ is less than or equal to the underlying filter of $g$ if and only if $f = g$.

Ultrafilter.coe_inj theorem

: (f : Filter α) = g ↔ f = g

Full source

@[simp, norm_cast]
theorem coe_inj : (f : Filter α) = g ↔ f = g :=
  coe_injective.eq_iff

Equality of Ultrafilters via Underlying Filter Equality

Informal description

For any two ultrafilters $f$ and $g$ on a type $\alpha$, the underlying filters of $f$ and $g$ are equal if and only if $f = g$.

Ultrafilter.ext theorem

⦃f g : Ultrafilter α⦄ (h : ∀ s, s ∈ f ↔ s ∈ g) : f = g

Full source

@[ext]
theorem ext ⦃f g : Ultrafilter α⦄ (h : ∀ s, s ∈ fs ∈ f ↔ s ∈ g) : f = g :=
  coe_injective <| Filter.ext h

Extensionality of Ultrafilters via Set Membership

Informal description

For any two ultrafilters $f$ and $g$ on a type $\alpha$, if for every set $s \subseteq \alpha$ we have $s \in f$ if and only if $s \in g$, then $f = g$.

Ultrafilter.le_of_inf_neBot theorem

(f : Ultrafilter α) {g : Filter α} (hg : NeBot (↑f ⊓ g)) : ↑f ≤ g

Full source

theorem le_of_inf_neBot (f : Ultrafilter α) {g : Filter α} (hg : NeBot (↑f ⊓ g)) : ↑f ≤ g :=
  le_of_inf_eq (f.unique inf_le_left hg)

Ultrafilter Order Relation via Non-Trivial Infimum

Informal description

Let $f$ be an ultrafilter on a type $\alpha$ and $g$ be a filter on $\alpha$. If the infimum of $f$ and $g$ is not the trivial filter (i.e., $\uparrow f \sqcap g \neq \bot$), then $f$ is less than or equal to $g$ in the filter order.

Ultrafilter.le_of_inf_neBot' theorem

(f : Ultrafilter α) {g : Filter α} (hg : NeBot (g ⊓ f)) : ↑f ≤ g

Full source

theorem le_of_inf_neBot' (f : Ultrafilter α) {g : Filter α} (hg : NeBot (g ⊓ f)) : ↑f ≤ g :=
  f.le_of_inf_neBot <| by rwa [inf_comm]

Ultrafilter Order Relation via Non-Trivial Infimum (Symmetric Version)

Informal description

Let $f$ be an ultrafilter on a type $\alpha$ and $g$ be a filter on $\alpha$. If the infimum of $g$ and $f$ is not the trivial filter (i.e., $g \sqcap f \neq \bot$), then $f$ is less than or equal to $g$ in the filter order.

Ultrafilter.inf_neBot_iff theorem

{f : Ultrafilter α} {g : Filter α} : NeBot (↑f ⊓ g) ↔ ↑f ≤ g

Full source

theorem inf_neBot_iff {f : Ultrafilter α} {g : Filter α} : NeBotNeBot (↑f ⊓ g) ↔ ↑f ≤ g :=
  ⟨le_of_inf_neBot f, fun h => (inf_of_le_left h).symm ▸ f.neBot⟩

Ultrafilter Infimum Nontriviality Criterion: $f \sqcap g \neq \bot \leftrightarrow f \leq g$

Informal description

For an ultrafilter $f$ on a type $\alpha$ and a filter $g$ on $\alpha$, the infimum $f \sqcap g$ is nontrivial (i.e., not equal to the bottom filter) if and only if $f \leq g$ in the filter order.

Ultrafilter.disjoint_iff_not_le theorem

{f : Ultrafilter α} {g : Filter α} : Disjoint (↑f) g ↔ ¬↑f ≤ g

Full source

theorem disjoint_iff_not_le {f : Ultrafilter α} {g : Filter α} : DisjointDisjoint (↑f) g ↔ ¬↑f ≤ g := by
  rw [← inf_neBot_iff, neBot_iff, Ne, not_not, disjoint_iff]

Ultrafilter Disjointness Criterion: $f \sqcap g = \bot \leftrightarrow f \nleq g$

Informal description

For an ultrafilter $f$ on a type $\alpha$ and a filter $g$ on $\alpha$, the filters $f$ and $g$ are disjoint (i.e., $f \sqcap g = \bot$) if and only if $f$ is not less than or equal to $g$ in the filter order.

Ultrafilter.compl_not_mem_iff theorem

: sᶜ ∉ f ↔ s ∈ f

Full source

@[simp]
theorem compl_not_mem_iff : sᶜsᶜ ∉ fsᶜ ∉ f ↔ s ∈ f :=
  ⟨fun hsc =>
    le_principal_iff.1 <|
      f.le_of_inf_neBot ⟨fun h => hsc <| mem_of_eq_bot <| by rwa [compl_compl]⟩,
    compl_not_mem⟩

Ultrafilter Complement Criterion: $s^\complement \notin f \leftrightarrow s \in f$

Informal description

For any ultrafilter $f$ on a type $\alpha$ and any subset $s \subseteq \alpha$, the complement $s^\complement$ is not in $f$ if and only if $s$ is in $f$.

Ultrafilter.frequently_iff_eventually theorem

: (∃ᶠ x in f, p x) ↔ ∀ᶠ x in f, p x

Full source

@[simp]
theorem frequently_iff_eventually : (∃ᶠ x in f, p x) ↔ ∀ᶠ x in f, p x :=
  compl_not_mem_iff

Ultrafilter Frequently-Eventually Equivalence: $(\exists^\infty x \in f, p(x)) \leftrightarrow (\forall^\infty x \in f, p(x))$

Informal description

For any ultrafilter $f$ on a type $\alpha$ and any predicate $p$ on $\alpha$, the statement "there exists a frequently occurring $x$ in $f$ such that $p(x)$ holds" is equivalent to "for all eventually occurring $x$ in $f$, $p(x)$ holds". In other words, $(\exists^\infty x \in f, p(x)) \leftrightarrow (\forall^\infty x \in f, p(x))$.

Ultrafilter.compl_mem_iff_not_mem theorem

: sᶜ ∈ f ↔ s ∉ f

Full source

theorem compl_mem_iff_not_mem : sᶜsᶜ ∈ fsᶜ ∈ f ↔ s ∉ f := by rw [← compl_not_mem_iff, compl_compl]

Ultrafilter Complement Membership Criterion: $s^\complement \in f \leftrightarrow s \notin f$

Informal description

For any ultrafilter $f$ on a type $\alpha$ and any subset $s \subseteq \alpha$, the complement $s^\complement$ is in $f$ if and only if $s$ is not in $f$.

Ultrafilter.diff_mem_iff theorem

(f : Ultrafilter α) : s \ t ∈ f ↔ s ∈ f ∧ t ∉ f

Full source

theorem diff_mem_iff (f : Ultrafilter α) : s \ ts \ t ∈ fs \ t ∈ f ↔ s ∈ f ∧ t ∉ f :=
  inter_mem_iff.trans <| and_congr Iff.rfl compl_mem_iff_not_mem

Ultrafilter Set Difference Membership Criterion: $s \setminus t \in f \leftrightarrow (s \in f \land t \notin f)$

Informal description

For any ultrafilter $f$ on a type $\alpha$ and any subsets $s, t \subseteq \alpha$, the set difference $s \setminus t$ belongs to $f$ if and only if $s$ belongs to $f$ and $t$ does not belong to $f$.

Ultrafilter.ofComplNotMemIff definition

(f : Filter α) (h : ∀ s, sᶜ ∉ f ↔ s ∈ f) : Ultrafilter α

Full source

/-- If `sᶜ ∉ f ↔ s ∈ f`, then `f` is an ultrafilter. The other implication is given by
`Ultrafilter.compl_not_mem_iff`. -/
def ofComplNotMemIff (f : Filter α) (h : ∀ s, sᶜsᶜ ∉ fsᶜ ∉ f ↔ s ∈ f) : Ultrafilter α where
  toFilter := f
  neBot' := ⟨fun hf => by simp [hf] at h⟩
  le_of_le _ _ hgf s hs := (h s).1 fun hsc => compl_not_mem hs (hgf hsc)

Ultrafilter construction from complement condition

Informal description

Given a filter $f$ on a type $\alpha$ such that for any set $s$, the complement $s^c$ is not in $f$ if and only if $s$ is in $f$, then $f$ is an ultrafilter. This construction provides a way to define an ultrafilter from a filter satisfying this complement condition.

Ultrafilter.ofAtom definition

(f : Filter α) (hf : IsAtom f) : Ultrafilter α

Full source

/-- If `f : Filter α` is an atom, then it is an ultrafilter. -/
def ofAtom (f : Filter α) (hf : IsAtom f) : Ultrafilter α where
  toFilter := f
  neBot' := ⟨hf.1⟩
  le_of_le g hg := (isAtom_iff_le_of_ge.1 hf).2 g hg.ne

Ultrafilter construction from an atomic filter

Informal description

Given a filter $f$ on a type $\alpha$ that is an atom in the lattice of filters (i.e., it is a minimal non-trivial filter), then $f$ is an ultrafilter. The construction `Ultrafilter.ofAtom` takes such a filter $f$ and a proof that it is an atom, and returns the corresponding ultrafilter structure.

Ultrafilter.nonempty_of_mem theorem

(hs : s ∈ f) : s.Nonempty

Full source

theorem nonempty_of_mem (hs : s ∈ f) : s.Nonempty :=
  Filter.nonempty_of_mem hs

Nonemptiness of Sets in an Ultrafilter

Informal description

For any set $s$ in an ultrafilter $f$ on a type $\alpha$, the set $s$ is nonempty. That is, if $s \in f$, then there exists an element $x \in \alpha$ such that $x \in s$.

Ultrafilter.ne_empty_of_mem theorem

(hs : s ∈ f) : s ≠ ∅

Full source

theorem ne_empty_of_mem (hs : s ∈ f) : s ≠ ∅ :=
  (nonempty_of_mem hs).ne_empty

Nonemptiness of Sets in an Ultrafilter

Informal description

For any set $s$ in an ultrafilter $f$ on a type $\alpha$, the set $s$ is nonempty, i.e., $s \neq \emptyset$.

Ultrafilter.empty_not_mem theorem

: ∅ ∉ f

Full source

@[simp]
theorem empty_not_mem : ∅∅ ∉ f :=
  Filter.empty_not_mem (f : Filter α)

Empty Set Not in Ultrafilter

Informal description

For any ultrafilter $f$ on a type $\alpha$, the empty set $\emptyset$ is not a member of $f$.

Ultrafilter.le_sup_iff theorem

{u : Ultrafilter α} {f g : Filter α} : ↑u ≤ f ⊔ g ↔ ↑u ≤ f ∨ ↑u ≤ g

Full source

@[simp]
theorem le_sup_iff {u : Ultrafilter α} {f g : Filter α} : ↑u ≤ f ⊔ g ↔ ↑u ≤ f ∨ ↑u ≤ g :=
  not_iff_not.1 <| by simp only [← disjoint_iff_not_le, not_or, disjoint_sup_right]

Ultrafilter Supremum Criterion: $u \leq f \sqcup g \leftrightarrow u \leq f \lor u \leq g$

Informal description

For any ultrafilter $u$ on a type $\alpha$ and any filters $f, g$ on $\alpha$, the ultrafilter $u$ is less than or equal to the supremum $f \sqcup g$ if and only if $u$ is less than or equal to $f$ or $u$ is less than or equal to $g$.

Ultrafilter.union_mem_iff theorem

: s ∪ t ∈ f ↔ s ∈ f ∨ t ∈ f

Full source

@[simp]
theorem union_mem_iff : s ∪ ts ∪ t ∈ fs ∪ t ∈ f ↔ s ∈ f ∨ t ∈ f := by
  simp only [← mem_coe, ← le_principal_iff, ← sup_principal, le_sup_iff]

Ultrafilter Union Membership Criterion: $s \cup t \in f \leftrightarrow s \in f \lor t \in f$

Informal description

For any ultrafilter $f$ on a type $\alpha$ and any sets $s, t \subseteq \alpha$, the union $s \cup t$ belongs to $f$ if and only if either $s$ belongs to $f$ or $t$ belongs to $f$.

Ultrafilter.mem_or_compl_mem theorem

(f : Ultrafilter α) (s : Set α) : s ∈ f ∨ sᶜ ∈ f

Full source

theorem mem_or_compl_mem (f : Ultrafilter α) (s : Set α) : s ∈ fs ∈ f ∨ sᶜ ∈ f :=
  or_iff_not_imp_left.2 compl_mem_iff_not_mem.2

Ultrafilter Dichotomy: $s \in f \lor s^\complement \in f$

Informal description

For any ultrafilter $f$ on a type $\alpha$ and any subset $s \subseteq \alpha$, either $s$ belongs to $f$ or its complement $s^\complement$ belongs to $f$.

Ultrafilter.em theorem

(f : Ultrafilter α) (p : α → Prop) : (∀ᶠ x in f, p x) ∨ ∀ᶠ x in f, ¬p x

Full source

protected theorem em (f : Ultrafilter α) (p : α → Prop) : (∀ᶠ x in f, p x) ∨ ∀ᶠ x in f, ¬p x :=
  f.mem_or_compl_mem { x | p x }

Ultrafilter Law of Excluded Middle: $(\forall^f x, p x) \lor (\forall^f x, \neg p x)$

Informal description

For any ultrafilter $f$ on a type $\alpha$ and any predicate $p : \alpha \to \text{Prop}$, either $p(x)$ holds for $f$-almost every $x \in \alpha$, or $\neg p(x)$ holds for $f$-almost every $x \in \alpha$.

Ultrafilter.eventually_or theorem

: (∀ᶠ x in f, p x ∨ q x) ↔ (∀ᶠ x in f, p x) ∨ ∀ᶠ x in f, q x

Full source

theorem eventually_or : (∀ᶠ x in f, p x ∨ q x) ↔ (∀ᶠ x in f, p x) ∨ ∀ᶠ x in f, q x :=
  union_mem_iff

Ultrafilter Disjunction Equivalence: $(∀^f x, p x ∨ q x) ↔ (∀^f x, p x) ∨ (∀^f x, q x)$

Informal description

For an ultrafilter $f$ on a type $\alpha$ and predicates $p, q : \alpha \to \text{Prop}$, the following are equivalent: 1. The statement $p(x) \lor q(x)$ holds for $f$-almost every $x \in \alpha$. 2. Either $p(x)$ holds for $f$-almost every $x \in \alpha$, or $q(x)$ holds for $f$-almost every $x \in \alpha$.

Ultrafilter.eventually_not theorem

: (∀ᶠ x in f, ¬p x) ↔ ¬∀ᶠ x in f, p x

Full source

theorem eventually_not : (∀ᶠ x in f, ¬p x) ↔ ¬∀ᶠ x in f, p x :=
  compl_mem_iff_not_mem

Ultrafilter Negation Equivalence: $(\forall^f x, \neg p x) \leftrightarrow \neg (\forall^f x, p x)$

Informal description

For any ultrafilter $f$ on a type $\alpha$ and any predicate $p : \alpha \to \text{Prop}$, the following are equivalent: 1. The statement $\neg p(x)$ holds for $f$-almost every $x \in \alpha$. 2. It is not the case that $p(x)$ holds for $f$-almost every $x \in \alpha$.

Ultrafilter.eventually_imp theorem

: (∀ᶠ x in f, p x → q x) ↔ (∀ᶠ x in f, p x) → ∀ᶠ x in f, q x

Full source

theorem eventually_imp : (∀ᶠ x in f, p x → q x) ↔ (∀ᶠ x in f, p x) → ∀ᶠ x in f, q x := by
  simp only [imp_iff_not_or, eventually_or, eventually_not]

Ultrafilter Implication Equivalence

Informal description

For an ultrafilter $f$ on a type $\alpha$ and predicates $p, q : \alpha \to \text{Prop}$, the following are equivalent: 1. The statement $p(x) \to q(x)$ holds for $f$-almost every $x \in \alpha$. 2. If $p(x)$ holds for $f$-almost every $x \in \alpha$, then $q(x)$ holds for $f$-almost every $x \in \alpha$.

Ultrafilter.map definition

(m : α → β) (f : Ultrafilter α) : Ultrafilter β

Full source

/-- Pushforward for ultrafilters. -/
nonrec def map (m : α → β) (f : Ultrafilter α) : Ultrafilter β :=
  ofComplNotMemIff (map m f) fun s => @compl_not_mem_iff _ f (m ⁻¹' s)

Pushforward of an ultrafilter

Informal description

Given a function $m : \alpha \to \beta$ and an ultrafilter $f$ on $\alpha$, the pushforward `map m f` is an ultrafilter on $\beta$ defined by the condition that a set $s \subseteq \beta$ is in `map m f` if and only if its preimage $m^{-1}(s)$ is in $f$.

Ultrafilter.coe_map theorem

(m : α → β) (f : Ultrafilter α) : (map m f : Filter β) = Filter.map m ↑f

Full source

@[simp, norm_cast]
theorem coe_map (m : α → β) (f : Ultrafilter α) : (map m f : Filter β) = Filter.map m ↑f :=
  rfl

Pushforward of Ultrafilter as Filter Equals Pushforward of Underlying Filter

Informal description

For any function $m : \alpha \to \beta$ and any ultrafilter $f$ on $\alpha$, the underlying filter of the pushforward `map m f` is equal to the pushforward of the underlying filter of $f$ under $m$. In other words, $(map\ m\ f : Filter\ \beta) = Filter.map\ m\ f$.

Ultrafilter.mem_map theorem

{m : α → β} {f : Ultrafilter α} {s : Set β} : s ∈ map m f ↔ m ⁻¹' s ∈ f

Full source

@[simp]
theorem mem_map {m : α → β} {f : Ultrafilter α} {s : Set β} : s ∈ map m fs ∈ map m f ↔ m ⁻¹' s ∈ f :=
  Iff.rfl

Characterization of Pushforward Ultrafilter Membership via Preimage

Informal description

For any function $m : \alpha \to \beta$, any ultrafilter $f$ on $\alpha$, and any subset $s \subseteq \beta$, the set $s$ belongs to the pushforward ultrafilter $\text{map}\, m\, f$ if and only if the preimage $m^{-1}(s)$ belongs to $f$.

Ultrafilter.map_id theorem

(f : Ultrafilter α) : f.map id = f

Full source

@[simp]
nonrec theorem map_id (f : Ultrafilter α) : f.map id = f :=
  coe_injective map_id

Identity Map Preserves Ultrafilter

Informal description

For any ultrafilter $f$ on a type $\alpha$, the pushforward of $f$ under the identity map $\mathrm{id} : \alpha \to \alpha$ is equal to $f$ itself, i.e., $f.\mathrm{map}(\mathrm{id}) = f$.

Ultrafilter.map_id' theorem

(f : Ultrafilter α) : (f.map fun x => x) = f

Full source

@[simp]
theorem map_id' (f : Ultrafilter α) : (f.map fun x => x) = f :=
  map_id _

Identity Function Preserves Ultrafilter under Pushforward

Informal description

For any ultrafilter $f$ on a type $\alpha$, the pushforward of $f$ under the identity function $\lambda x, x$ is equal to $f$ itself, i.e., $f.\mathrm{map}(\lambda x, x) = f$.

Ultrafilter.map_map theorem

(f : Ultrafilter α) (m : α → β) (n : β → γ) : (f.map m).map n = f.map (n ∘ m)

Full source

@[simp]
nonrec theorem map_map (f : Ultrafilter α) (m : α → β) (n : β → γ) :
  (f.map m).map n = f.map (n ∘ m) :=
  coe_injective map_map

Composition Law for Pushforward of Ultrafilters

Informal description

For any ultrafilter $f$ on a type $\alpha$ and functions $m : \alpha \to \beta$ and $n : \beta \to \gamma$, the pushforward of $f$ along $n$ after pushing forward along $m$ is equal to the pushforward of $f$ along the composition $n \circ m$. In other words, $(f.\text{map}\, m).\text{map}\, n = f.\text{map}\, (n \circ m)$.

Ultrafilter.comap definition

{m : α → β} (u : Ultrafilter β) (inj : Injective m) (large : Set.range m ∈ u) : Ultrafilter α

Full source

/-- The pullback of an ultrafilter along an injection whose range is large with respect to the given
ultrafilter. -/
nonrec def comap {m : α → β} (u : Ultrafilter β) (inj : Injective m) (large : Set.rangeSet.range m ∈ u) :
    Ultrafilter α where
  toFilter := comap m u
  neBot' := u.neBot'.comap_of_range_mem large
  le_of_le g hg hgu := by
    simp only [← u.unique (map_le_iff_le_comap.2 hgu), comap_map inj, le_rfl]

Pullback of an ultrafilter along an injective function

Informal description

Given an injective function $ m : \alpha \to \beta $, an ultrafilter $ u $ on $ \beta $, and the assumption that the range of $ m $ is a member of $ u $, the operation `Ultrafilter.comap` constructs an ultrafilter on $ \alpha $ by pulling back $ u $ along $ m $. This ultrafilter consists of all sets $ s \subseteq \alpha $ such that the image $ m(s) $ is a member of $ u $.

Ultrafilter.mem_comap theorem

 {m : α → β} (u : Ultrafilter β) (inj : Injective m) (large : Set.range m ∈ u) {s : Set α} :
  s ∈ u.comap inj large ↔ m '' s ∈ u

Full source

@[simp]
theorem mem_comap {m : α → β} (u : Ultrafilter β) (inj : Injective m) (large : Set.rangeSet.range m ∈ u)
    {s : Set α} : s ∈ u.comap inj larges ∈ u.comap inj large ↔ m '' s ∈ u :=
  mem_comap_iff inj large

Membership Criterion for Pullback Ultrafilter via Image

Informal description

Let $m : \alpha \to \beta$ be an injective function, $u$ an ultrafilter on $\beta$ such that the range of $m$ is in $u$, and $s$ a subset of $\alpha$. Then $s$ is a member of the pullback ultrafilter $u.\text{comap}\, m$ if and only if the image $m(s)$ is a member of $u$.

Ultrafilter.coe_comap theorem

 {m : α → β} (u : Ultrafilter β) (inj : Injective m) (large : Set.range m ∈ u) :
  (u.comap inj large : Filter α) = Filter.comap m u

Full source

@[simp, norm_cast]
theorem coe_comap {m : α → β} (u : Ultrafilter β) (inj : Injective m) (large : Set.rangeSet.range m ∈ u) :
    (u.comap inj large : Filter α) = Filter.comap m u :=
  rfl

Underlying Filter of Pullback Ultrafilter Equals Filter Pullback

Informal description

Let $m : \alpha \to \beta$ be an injective function, $u$ an ultrafilter on $\beta$ such that the range of $m$ is in $u$. Then the underlying filter of the pullback ultrafilter $u.\text{comap}\, m$ (constructed via `Ultrafilter.comap`) is equal to the filter pullback $\text{Filter.comap}\, m\, u$.

Ultrafilter.instPure instance

: Pure Ultrafilter

Full source

/-- The principal ultrafilter associated to a point `x`. -/
instance : Pure Ultrafilter :=
  ⟨fun a => ofComplNotMemIff (pure a) fun s => by simp⟩

Principal Ultrafilter Construction

Informal description

For any type $\alpha$, there is a canonical way to construct an ultrafilter from any element $x \in \alpha$, called the principal ultrafilter at $x$. This ultrafilter consists of all subsets of $\alpha$ that contain $x$.

Ultrafilter.mem_pure theorem

{a : α} {s : Set α} : s ∈ (pure a : Ultrafilter α) ↔ a ∈ s

Full source

@[simp]
theorem mem_pure {a : α} {s : Set α} : s ∈ (pure a : Ultrafilter α)s ∈ (pure a : Ultrafilter α) ↔ a ∈ s :=
  Iff.rfl

Membership in Principal Ultrafilter: $s \in \text{pure}(a) \leftrightarrow a \in s$

Informal description

For any element $a$ of type $\alpha$ and any set $s \subseteq \alpha$, the set $s$ belongs to the principal ultrafilter generated by $a$ if and only if $a$ is an element of $s$. In other words, $s \in \text{pure}(a) \leftrightarrow a \in s$.

Ultrafilter.coe_pure theorem

(a : α) : ↑(pure a : Ultrafilter α) = (pure a : Filter α)

Full source

@[simp]
theorem coe_pure (a : α) : ↑(pure a : Ultrafilter α) = (pure a : Filter α) :=
  rfl

Coercion of Principal Ultrafilter to Principal Filter

Informal description

For any element $a$ of type $\alpha$, the underlying filter of the principal ultrafilter generated by $a$ is equal to the principal filter generated by $a$. In other words, the coercion of the principal ultrafilter at $a$ to a filter is the principal filter at $a$.

Ultrafilter.map_pure theorem

(m : α → β) (a : α) : map m (pure a) = pure (m a)

Full source

@[simp]
theorem map_pure (m : α → β) (a : α) : map m (pure a) = pure (m a) :=
  rfl

Pushforward of Principal Ultrafilter Equals Principal Ultrafilter of Image

Informal description

For any function $m : \alpha \to \beta$ and any element $a \in \alpha$, the pushforward of the principal ultrafilter at $a$ under $m$ is equal to the principal ultrafilter at $m(a)$. In other words, $\text{map}\, m\, (\text{pure}\, a) = \text{pure}\, (m\, a)$.

Ultrafilter.comap_pure theorem

{m : α → β} (a : α) (inj : Injective m) (large) : comap (pure <| m a) inj large = pure a

Full source

@[simp]
theorem comap_pure {m : α → β} (a : α) (inj : Injective m) (large) :
    comap (pure <| m a) inj large = pure a :=
  coe_injective <|
    Filter.comap_pure.trans <| by
      rw [coe_pure, ← principal_singleton, ← image_singleton, preimage_image_eq _ inj]

Pullback of Principal Ultrafilter along Injective Function Equals Principal Ultrafilter

Informal description

Let $m : \alpha \to \beta$ be an injective function and $a \in \alpha$. For any ultrafilter $u$ on $\beta$ such that the range of $m$ is in $u$, the pullback of the principal ultrafilter at $m(a)$ along $m$ is equal to the principal ultrafilter at $a$. That is, $\text{comap}\, m\, (\text{pure}\, (m\, a)) = \text{pure}\, a$.

Ultrafilter.pure_injective theorem

: Injective (pure : α → Ultrafilter α)

Full source

theorem pure_injective : Injective (pure : α → Ultrafilter α) := fun _ _ h =>
  Filter.pure_injective (congr_arg Ultrafilter.toFilter h :)

Injectivity of Principal Ultrafilter Construction

Informal description

The function $\text{pure} : \alpha \to \text{Ultrafilter} \alpha$, which maps each element $x \in \alpha$ to the principal ultrafilter generated by $x$, is injective. That is, for any $x, y \in \alpha$, if $\text{pure}(x) = \text{pure}(y)$, then $x = y$.

Ultrafilter.instInhabited instance

[Inhabited α] : Inhabited (Ultrafilter α)

Full source

instance [Inhabited α] : Inhabited (Ultrafilter α) :=
  ⟨pure default⟩

Ultrafilters on Inhabited Types are Inhabited

Informal description

For any inhabited type $\alpha$, the type of ultrafilters on $\alpha$ is also inhabited.

Ultrafilter.instNonempty instance

[Nonempty α] : Nonempty (Ultrafilter α)

Full source

instance [Nonempty α] : Nonempty (Ultrafilter α) :=
  Nonempty.map pure inferInstance

Existence of Ultrafilters on Nonempty Types

Informal description

For any nonempty type $\alpha$, there exists an ultrafilter on $\alpha$.

Ultrafilter.bind definition

(f : Ultrafilter α) (m : α → Ultrafilter β) : Ultrafilter β

Full source

/-- Monadic bind for ultrafilters, coming from the one on filters
defined in terms of map and join. -/
def bind (f : Ultrafilter α) (m : α → Ultrafilter β) : Ultrafilter β :=
  ofComplNotMemIff (Filter.bind ↑f fun x => ↑(m x)) fun s => by
    simp only [mem_bind', mem_coe, ← compl_mem_iff_not_mem, compl_setOf, compl_compl]

Ultrafilter bind operation

Informal description

Given an ultrafilter $ f $ on a type $ \alpha $ and a function $ m $ mapping each element of $ \alpha $ to an ultrafilter on $ \beta $, the operation `Ultrafilter.bind` constructs a new ultrafilter on $ \beta $. This is defined as the ultrafilter generated by the filter bind operation applied to $ f $ and $ m $, ensuring that for any set $ s $, the complement of $ s $ is not in the resulting ultrafilter if and only if $ s $ is in it.

Ultrafilter.instBind instance

: Bind Ultrafilter

Full source

instance instBind : Bind Ultrafilter :=
  ⟨@Ultrafilter.bind⟩

Ultrafilter Bind Operation

Informal description

The ultrafilter type constructor admits a bind operation, making it an instance of the `Bind` typeclass. Specifically, for any types $\alpha$ and $\beta$, given an ultrafilter $f$ on $\alpha$ and a function $m : \alpha \to \text{Ultrafilter} \beta$, the bind operation constructs a new ultrafilter on $\beta$ by combining $f$ and $m$ in the canonical way.

Ultrafilter.functor instance

: Functor Ultrafilter

Full source

instance functor : Functor Ultrafilter where map := @Ultrafilter.map

Ultrafilter Functoriality

Informal description

The ultrafilter construction forms a functor, meaning that for any types $\alpha$ and $\beta$, a function $f : \alpha \to \beta$ induces a map `Ultrafilter.map f : Ultrafilter \alpha \to Ultrafilter \beta` that preserves identity and composition.

Ultrafilter.monad instance

: Monad Ultrafilter

Full source

instance monad : Monad Ultrafilter where map := @Ultrafilter.map

Monad Structure on Ultrafilters

Informal description

The type constructor `Ultrafilter` forms a monad, meaning it is equipped with a pure operation (constructing principal ultrafilters) and a bind operation (combining ultrafilters through functions to ultrafilters), satisfying the monad laws.

Ultrafilter.lawfulMonad instance

: LawfulMonad Ultrafilter

Full source

instance lawfulMonad : LawfulMonad Ultrafilter where
  id_map f := coe_injective (id_map f.toFilter)
  pure_bind a f := coe_injective (Filter.pure_bind a ((Ultrafilter.toFilter) ∘ f))
  bind_assoc _ _ _ := coe_injective (filter_eq rfl)
  bind_pure_comp f x := coe_injective (bind_pure_comp f x.1)
  map_const := rfl
  seqLeft_eq _ _ := rfl
  seqRight_eq _ _ := rfl
  pure_seq _ _ := rfl
  bind_map _ _ := rfl

Ultrafilter Monad Laws

Informal description

The monad structure on ultrafilters satisfies the monad laws, meaning the operations of pure (constructing principal ultrafilters) and bind (combining ultrafilters through functions to ultrafilters) are well-behaved with respect to identity and composition.

Ultrafilter.exists_le theorem

(f : Filter α) [h : NeBot f] : ∃ u : Ultrafilter α, ↑u ≤ f

Full source

/-- The ultrafilter lemma: Any proper filter is contained in an ultrafilter. -/
theorem exists_le (f : Filter α) [h : NeBot f] : ∃ u : Ultrafilter α, ↑u ≤ f :=
  let ⟨u, hu, huf⟩ := (eq_bot_or_exists_atom_le f).resolve_left h.ne
  ⟨ofAtom u hu, huf⟩

Existence of Ultrafilter Extending a Proper Filter

Informal description

For any proper filter $f$ on a type $\alpha$, there exists an ultrafilter $u$ on $\alpha$ such that $u \leq f$ in the inclusion order.

Ultrafilter.of definition

(f : Filter α) [NeBot f] : Ultrafilter α

Full source

/-- 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. -/
noncomputable def of (f : Filter α) [NeBot f] : Ultrafilter α :=
  Classical.choose (exists_le f)

Ultrafilter extending a given filter

Informal description

Given a proper filter $f$ on a type $\alpha$, the function `Ultrafilter.of` constructs an ultrafilter that extends $f$, i.e., an ultrafilter $u$ such that $u \leq f$ in the inclusion order. The existence of such an ultrafilter is guaranteed by the ultrafilter lemma, which is proved using the axiom of choice.

Ultrafilter.of_le theorem

(f : Filter α) [NeBot f] : ↑(of f) ≤ f

Full source

theorem of_le (f : Filter α) [NeBot f] : ↑(of f) ≤ f :=
  Classical.choose_spec (exists_le f)

Ultrafilter Extension Property: $\text{of}(f) \leq f$

Informal description

For any proper filter $f$ on a type $\alpha$, the ultrafilter $\text{of}(f)$ constructed from $f$ satisfies $\text{of}(f) \leq f$ in the inclusion order.

Ultrafilter.of_coe theorem

(f : Ultrafilter α) : of ↑f = f

Full source

theorem of_coe (f : Ultrafilter α) : of ↑f = f :=
  coe_inj.1 <| f.unique (of_le f.toFilter)

Ultrafilter Construction from Underlying Filter is Identity

Informal description

For any ultrafilter $f$ on a type $\alpha$, the ultrafilter constructed from the underlying filter of $f$ via `Ultrafilter.of` is equal to $f$ itself, i.e., $\text{of}(f) = f$.

Filter.isAtom_pure theorem

: IsAtom (pure a : Filter α)

Full source

theorem isAtom_pure : IsAtom (pure a : Filter α) :=
  (pure a : Ultrafilter α).isAtom

Principal Filters are Atoms in the Filter Lattice

Informal description

For any element $a$ in a type $\alpha$, the principal filter $\text{pure}(a)$ is an atom in the lattice of filters on $\alpha$. That is, $\text{pure}(a) \neq \bot$ and for any filter $f$ on $\alpha$, if $f \leq \text{pure}(a)$, then either $f = \bot$ or $f = \text{pure}(a)$.

Filter.NeBot.le_pure_iff theorem

(hf : f.NeBot) : f ≤ pure a ↔ f = pure a

Full source

protected theorem NeBot.le_pure_iff (hf : f.NeBot) : f ≤ pure a ↔ f = pure a :=
  ⟨Ultrafilter.unique (pure a), le_of_eq⟩

Characterization of Principal Ultrafilters: $f \leq \text{pure}(a) \leftrightarrow f = \text{pure}(a)$ for Non-Trivial Filters

Informal description

For any non-trivial filter $f$ (i.e., $f$ is not the trivial filter) on a type $\alpha$, and for any element $a \in \alpha$, the filter $f$ is less than or equal to the principal ultrafilter at $a$ if and only if $f$ is equal to the principal ultrafilter at $a$. In other words, $f \leq \text{pure}(a) \leftrightarrow f = \text{pure}(a)$.

Filter.lt_pure_iff theorem

: f < pure a ↔ f = ⊥

Full source

@[simp]
theorem lt_pure_iff : f < pure a ↔ f = ⊥ :=
  isAtom_pure.lt_iff

Characterization of Filters Strictly Below a Principal Ultrafilter: $f < \text{pure}(a) \leftrightarrow f = \bot$

Informal description

For any filter $f$ on a type $\alpha$ and any element $a \in \alpha$, the filter $f$ is strictly less than the principal ultrafilter $\text{pure}(a)$ if and only if $f$ is the trivial filter $\bot$.

Filter.le_pure_iff' theorem

: f ≤ pure a ↔ f = ⊥ ∨ f = pure a

Full source

theorem le_pure_iff' : f ≤ pure a ↔ f = ⊥ ∨ f = pure a :=
  isAtom_pure.le_iff

Characterization of Filters Below Principal Filter: $f \leq \text{pure}(a) \leftrightarrow f = \bot \lor f = \text{pure}(a)$

Informal description

A filter $f$ on a type $\alpha$ is less than or equal to the principal filter $\text{pure}(a)$ for some $a \in \alpha$ if and only if $f$ is the bottom filter $\bot$ or $f$ equals $\text{pure}(a)$.

Filter.Iic_pure theorem

(a : α) : Iic (pure a : Filter α) = {⊥, pure a}

Full source

@[simp]
theorem Iic_pure (a : α) : Iic (pure a : Filter α) = {⊥, pure a} :=
  isAtom_pure.Iic_eq

Characterization of Filters Below Principal Filter: $\text{Iic}(\text{pure}(a)) = \{\bot, \text{pure}(a)\}$

Informal description

For any element $a$ in a type $\alpha$, the set of all filters on $\alpha$ that are less than or equal to the principal filter $\text{pure}(a)$ is exactly $\{\bot, \text{pure}(a)\}$, where $\bot$ is the trivial filter.

Filter.mem_iff_ultrafilter theorem

: s ∈ f ↔ ∀ g : Ultrafilter α, ↑g ≤ f → s ∈ g

Full source

theorem mem_iff_ultrafilter : s ∈ fs ∈ f ↔ ∀ g : Ultrafilter α, ↑g ≤ f → s ∈ g := by
  refine ⟨fun hf g hg => hg hf, fun H => by_contra fun hf => ?_⟩
  set g : Filter (sᶜ : Set α) := comap (↑) f
  haveI : NeBot g := comap_neBot_iff_compl_range.2 (by simpa [compl_setOf] )
  simpa using H ((of g).map (↑)) (map_le_iff_le_comap.mpr (of_le g))

Ultrafilter Characterization of Filter Membership: $s \in f \leftrightarrow \forall g \leq f, s \in g$

Informal description

A set $s$ belongs to a filter $f$ on a type $\alpha$ if and only if for every ultrafilter $g$ on $\alpha$ such that $g \leq f$, the set $s$ belongs to $g$.

Filter.le_iff_ultrafilter theorem

{f₁ f₂ : Filter α} : f₁ ≤ f₂ ↔ ∀ g : Ultrafilter α, ↑g ≤ f₁ → ↑g ≤ f₂

Full source

theorem le_iff_ultrafilter {f₁ f₂ : Filter α} : f₁ ≤ f₂ ↔ ∀ g : Ultrafilter α, ↑g ≤ f₁ → ↑g ≤ f₂ :=
  ⟨fun h _ h₁ => h₁.trans h, fun h _ hs => mem_iff_ultrafilter.2 fun g hg => h g hg hs⟩

Ultrafilter Characterization of Filter Order: $f_1 \leq f_2 \leftrightarrow \forall g \leq f_1, g \leq f_2$

Informal description

For any two filters $f_1$ and $f_2$ on a type $\alpha$, $f_1$ is less than or equal to $f_2$ if and only if for every ultrafilter $g$ on $\alpha$ such that $g \leq f_1$, it also holds that $g \leq f_2$.

Filter.iSup_ultrafilter_le_eq theorem

(f : Filter α) : ⨆ (g : Ultrafilter α) (_ : g ≤ f), (g : Filter α) = f

Full source

/-- A filter equals the intersection of all the ultrafilters which contain it. -/
theorem iSup_ultrafilter_le_eq (f : Filter α) :
    ⨆ (g : Ultrafilter α) (_ : g ≤ f), (g : Filter α) = f :=
  eq_of_forall_ge_iff fun f' => by simp only [iSup_le_iff, ← le_iff_ultrafilter]

Filter Decomposition via Ultrafilters: $\bigsqcup_{g \leq f} g = f$

Informal description

For any filter $f$ on a type $\alpha$, the supremum of all ultrafilters $g$ that are less than or equal to $f$ is equal to $f$ itself. In other words, \[ \bigsqcup_{\substack{g \text{ ultrafilter} \\ g \leq f}} g = f. \]

Filter.exists_ultrafilter_iff theorem

{f : Filter α} : (∃ u : Ultrafilter α, ↑u ≤ f) ↔ NeBot f

Full source

theorem exists_ultrafilter_iff {f : Filter α} : (∃ u : Ultrafilter α, ↑u ≤ f) ↔ NeBot f :=
  ⟨fun ⟨_, uf⟩ => neBot_of_le uf, fun h => @exists_ultrafilter_le _ _ h⟩

Existence of Ultrafilter Extension for Nontrivial Filters

Informal description

For any filter $f$ on a type $\alpha$, there exists an ultrafilter $u$ such that $u \leq f$ if and only if $f$ is a nontrivial filter (i.e., $f \neq \bot$).

Filter.forall_neBot_le_iff theorem

 {g : Filter α} {p : Filter α → Prop} (hp : Monotone p) :
  (∀ f : Filter α, NeBot f → f ≤ g → p f) ↔ ∀ f : Ultrafilter α, ↑f ≤ g → p f

Full source

theorem forall_neBot_le_iff {g : Filter α} {p : Filter α → Prop} (hp : Monotone p) :
    (∀ f : Filter α, NeBot f → f ≤ g → p f) ↔ ∀ f : Ultrafilter α, ↑f ≤ g → p f := by
  refine ⟨fun H f hf => H f f.neBot hf, ?_⟩
  intro H f hf hfg
  exact hp (of_le f) (H _ ((of_le f).trans hfg))

Ultrafilter Characterization of Monotone Predicates: $\forall f \leq g, p(f) \leftrightarrow \forall \text{ultrafilters } f \leq g, p(f)$

Informal description

Let $g$ be a filter on a type $\alpha$ and $p$ be a monotone predicate on filters over $\alpha$. Then the following are equivalent: 1. For every nontrivial filter $f$ such that $f \leq g$, the predicate $p(f)$ holds. 2. For every ultrafilter $f$ such that $f \leq g$, the predicate $p(f)$ holds.

Ultrafilter.comap_inf_principal_neBot_of_image_mem theorem

(h : m '' s ∈ g) : (Filter.comap m g ⊓ 𝓟 s).NeBot

Full source

theorem comap_inf_principal_neBot_of_image_mem (h : m '' sm '' s ∈ g) : (Filter.comapFilter.comap m g ⊓ 𝓟 s).NeBot :=
  Filter.comap_inf_principal_neBot_of_image_mem g.neBot h

Nontriviality of Comap Inf Principal Filter under Image Membership

Informal description

Let $g$ be an ultrafilter on a type $\beta$, $m : \alpha \to \beta$ a function, and $s \subseteq \alpha$ a subset. If the image $m(s)$ belongs to $g$, then the filter obtained by taking the infimum of the comap filter $\text{comap}\, m\, g$ and the principal filter $\mathfrak{P}(s)$ is nontrivial (i.e., not equal to the bottom filter).

Ultrafilter.ofComapInfPrincipal definition

(h : m '' s ∈ g) : Ultrafilter α

Full source

/-- Ultrafilter extending the inf of a comapped ultrafilter and a principal ultrafilter. -/
noncomputable def ofComapInfPrincipal (h : m '' sm '' s ∈ g) : Ultrafilter α :=
  @of _ (Filter.comapFilter.comap m g ⊓ 𝓟 s) (comap_inf_principal_neBot_of_image_mem h)

Ultrafilter extending comap inf principal filter

Informal description

Given an ultrafilter $ g $ on a type $ \beta $, a function $ m : \alpha \to \beta $, and a subset $ s \subseteq \alpha $ such that the image $ m(s) $ belongs to $ g $, the function `Ultrafilter.ofComapInfPrincipal` constructs an ultrafilter on $ \alpha $ that extends the infimum of the comap filter $ \text{comap}\, m\, g $ and the principal filter generated by $ s $.

Ultrafilter.ofComapInfPrincipal_mem theorem

(h : m '' s ∈ g) : s ∈ ofComapInfPrincipal h

Full source

theorem ofComapInfPrincipal_mem (h : m '' sm '' s ∈ g) : s ∈ ofComapInfPrincipal h := by
  let f := Filter.comapFilter.comap m g ⊓ 𝓟 s
  haveI : f.NeBot := comap_inf_principal_neBot_of_image_mem h
  have : s ∈ f := mem_inf_of_right (mem_principal_self s)
  exact le_def.mp (of_le _) s this

Membership of $s$ in the Ultrafilter Constructed via Comap and Principal Filter

Informal description

Let $g$ be an ultrafilter on a type $\beta$, $m : \alpha \to \beta$ a function, and $s \subseteq \alpha$ a subset such that the image $m(s)$ belongs to $g$. Then the set $s$ is a member of the ultrafilter $\text{ofComapInfPrincipal}\, h$ constructed from $g$, $m$, and $s$.

Ultrafilter.ofComapInfPrincipal_eq_of_map theorem

(h : m '' s ∈ g) : (ofComapInfPrincipal h).map m = g

Full source

theorem ofComapInfPrincipal_eq_of_map (h : m '' sm '' s ∈ g) : (ofComapInfPrincipal h).map m = g := by
  let f := Filter.comapFilter.comap m g ⊓ 𝓟 s
  haveI : f.NeBot := comap_inf_principal_neBot_of_image_mem h
  apply eq_of_le
  calc
    Filter.map m (of f) ≤ Filter.map m f := map_mono (of_le _)
    _ ≤ (Filter.map m <| Filter.comap m g) ⊓ Filter.map m (𝓟 s) := map_inf_le
    _ = (Filter.map m <| Filter.comap m g) ⊓ (𝓟 <| m '' s) := by rw [map_principal]
    _ ≤ ↑g ⊓ (𝓟 <| m '' s) := inf_le_inf_right _ map_comap_le
    _ = ↑g := inf_of_le_left (le_principal_iff.mpr h)

Pushforward of Ultrafilter Extension Equals Original Ultrafilter

Informal description

Let $g$ be an ultrafilter on a type $\beta$, $m : \alpha \to \beta$ a function, and $s \subseteq \alpha$ a subset such that the image $m(s)$ belongs to $g$. Then the pushforward of the ultrafilter $\text{ofComapInfPrincipal}\, h$ under $m$ equals $g$, i.e., $(\text{ofComapInfPrincipal}\, h).\text{map}\, m = g$.