coe_pure — Mathlib

English

The underlying Filter of the principal ultrafilter at a coincides with the principal filter at a.

Русский

Основа фильтра главного ультрафильтра в точке a совпадает с главной фильтрацией в точке a.

LaTeX

$$$ \uparrow(\text{pure } a : Ultrafilter \alpha) = (\text{pure } a : Filter \alpha) $$$

Lean4

@[simp]
theorem coe_pure (a : α) : ↑(pure a : Ultrafilter α) = (pure a : Filter α) :=
  rfl

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