coe_inj — Mathlib

English

Equality of ultrafilters is reflected by equality of their underlying filters.

Русский

Равенство ульрафильтров эквивалентно равенству их базовых фильтров.

LaTeX

$$$\\\\forall f,g \\\\in \\\\mathrm{Ultrafilter}(\\\\alpha), (f : \\\\mathrm{Filter}(\\\\alpha)) = (g : \\\\mathrm{Filter}(\\\\alpha)) \\\\Leftrightarrow f = g$$$

Lean4

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

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