mem_iff_ultrafilter — Mathlib

English

A set s is in a filter f if and only if, for every ultrafilter g below f, s ∈ g.

Русский

Множество s принадлежит фильтру f тогда и только тогда, когда для каждого ультрафильтра g ниже f, s ∈ g.

LaTeX

$$$ s \in f \iff \forall g : Ultrafilter α, g \le f \rightarrow s \in g $$$

Lean4

theorem mem_iff_ultrafilter : s ∈ 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))

Похожие утверждения