coe_of

Mathlib.Order.Category.NonemptyFinLinOrd

URI: https://scilib.ai/kg/mathlib#NonemptyFinLinOrd.coe_of

English

The carrier of NonemptyFinLinOrd.of α equals α for any nonempty, finite, linearly ordered α.

Русский

Носитель NonemptyFinLinOrd.of α равен α при любом непустом конечном линейном порядке α.

LaTeX

$$carrier(NonemptyFinLinOrd.of α) = α$$

Lean4

theorem coe_of (α : Type*) [Nonempty α] [Fintype α] [LinearOrder α] : ↥(of α) = α :=
  rfl

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

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

Разделы

Аффилиация

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