singletonOneHom — Mathlib

English

The singleton operation defines a OneHom from α to Set α, with toFun = singleton and map_one' = singleton_one.

Русский

Операция одиночного элемента задаёт гомоморфизму единицы из α в Set α, где отображение равно образованию единичного множества, и map_one совпадает с singleton_one.

LaTeX

$$singletonOneHom : OneHom α (Set α) where toFun := singleton; map_one' := singleton_one$$

Lean4

/-- The singleton operation as a `OneHom`. -/
@[to_additive /-- The singleton operation as a `ZeroHom`. -/
    ]
def singletonOneHom : OneHom α (Set α) where toFun := singleton; map_one' := singleton_one

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