ext — Mathlib

English

Two ultrafilters are equal if and only if they contain exactly the same sets.

Русский

Два ульрафильтра равны тогда и только тогда, когда содержат одни и те же множества.

LaTeX

$$$\\\\forall f,g \\\\in \\\\mathrm{Ultrafilter}(\\\\alpha), (\\\\forall S \\\\subseteq \\\\alpha, S \\\\in f \\\\Leftrightarrow S \\\\in g) \\\\Rightarrow f = g$$$

Lean4

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

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