coe_succOrderEmb

Mathlib.Order.Fin.Basic

URI: https://scilib.ai/kg/mathlib#Fin.coe_succOrderEmb

English

The coercion of the successor order embedding equals the standard successor function.

Русский

Ковариантность отображения-коэрцирования вложения успеха равна обычной функции следования.

LaTeX

$$$\forall {n : \mathbb{N}}, \; \mathrm{coe}(\mathrm{succOrderEmb}(n)) = \mathrm{Fin.succ}$$$

Lean4

@[simp, norm_cast]
theorem coe_succOrderEmb : ⇑(succOrderEmb n) = Fin.succ :=
  rfl

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

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

Разделы

Аффилиация

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