mk_coe

Mathlib.Data.Finset.Defs

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

English

The coercion from a subtype element to its value is compatible with the underlying element: (⟨x, h⟩ : (s : Set α)) = x.

Русский

Коэрцирование элемента подтипа к его значению согласовано: (⟨x, h⟩ : (s : Set α)) = x.

LaTeX

$$$ (\langle x, h \rangle : (s : Set \alpha)) = x $$$

Lean4

theorem mk_coe {s : Finset α} (x : (s : Set α)) {h} : (⟨x, h⟩ : (s : Set α)) = x :=
  Subtype.coe_eta _ _

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

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

Разделы

Аффилиация

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