coe_finsetEquivSet

Mathlib.Data.Fintype.Sets

URI: https://scilib.ai/kg/mathlib#Fintype.coe_finsetEquivSet

English

The forward map of finsetEquivSet is the inclusion map from Finset α to Set α.

Русский

Переходная карта финсет-эквиварианта является включением Finset α в Set α.

LaTeX

$$$\text{coe}_{\mathrm{finsetEquivSet}} = (↑) : \mathrm{Finset}\,\alpha \to \mathrm{Set}\,\alpha$$$

Lean4

@[simp, norm_cast]
theorem coe_finsetEquivSet : ⇑finsetEquivSet = ((↑) : Finset α → Set α) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru