pureOneHom — Mathlib

English

There exists a canonical OneHom from α to Filter α sending a ↦ pure a, i.e., pureOneHom is the natural embedding of α into Filter α.

Русский

Существует канонический OneHom из α в Filter α, отправляющий a ↦ pure a; то есть pureOneHom — естественное вложение α в Filter α.

LaTeX

$$$\\text{pureOneHom} : \\text{OneHom } \\alpha (\\text{Filter } \\alpha)$ with toFun(a) = \\mathrm{pure}(a)$$

Lean4

/-- `pure` as a `OneHom`. -/
@[to_additive /-- `pure` as a `ZeroHom`. -/
    ]
def pureOneHom : OneHom α (Filter α) where toFun := pure; map_one' := pure_one

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