coe_le_coe — Mathlib

English

The order (f : Filter α) ≤ g is equivalent to f = g for ultrafilters.

Русский

Порядок (f : Filter α) ≤ g эквивалентен f = g для ульрафильтров.

LaTeX

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

Lean4

@[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⟩

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