coe_injective — Mathlib

English

The map sending an ultrafilter to its underlying filter is injective; ultrafilters are determined by their associated filters.

Русский

Отображение ультрафильтра в связанный фильтр инъективно; ультрафильтры определяется их соответствующими фильтрами.

LaTeX

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

Lean4

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

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