coe_coeEmb

Mathlib.Data.Finset.Defs

URI: https://scilib.ai/kg/mathlib#Finset.coe_coeEmb

English

The underlying function of the natural embedding coincides with the canonical coercion.

Русский

Функция, лежащая в основе естественного вложения, совпадает с каноническим приводением.

LaTeX

$$$\text{coeEmb}^{\;\text{underlying}} = \text{(coercion to Set)}$$$

Lean4

@[simp]
theorem coe_coeEmb : ⇑(coeEmb : Finset α ↪o Set α) = ((↑) : Finset α → Set α) :=
  rfl

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

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

Разделы

Аффилиация

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