coe_coeMonoidHom — Mathlib

English

Let α be a type equipped with a monoïd structure. The canonical forgetful map from Finset α to Set α agrees with identifying each finite set with its underlying subset of α.

Русский

Пусть α — множество с моноидной структурой. Каноническое отображение забывания Finset α в Set α совпадает с естественной идентификацией каждого конечного множества с его подмножеством α.

LaTeX

$$$\\big(\\mathrm{coeMonoidHom} : \\mathrm{Finset}\\,\\alpha \\to \\mathrm{Set}\\,\\alpha\\big) = \\uparrow$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_coeMonoidHom : (coeMonoidHom : Finset α → Set α) = (↑) :=
  rfl

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