succOrderEmb_toEmbedding

Mathlib.Order.Fin.Basic

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

English

succOrderEmb n .toEmbedding equals succEmb n.

Русский

succOrderEmb(n).toEmbedding равняется succEmb(n).

LaTeX

$$$\forall {n : \mathbb{N}}, (\mathrm{succOrderEmb}(n)).toEmbedding = \mathrm{succEmb}(n)$$$

Lean4

@[simp]
theorem succOrderEmb_toEmbedding : (succOrderEmb n).toEmbedding = succEmb n :=
  rfl

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

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

Разделы

Аффилиация

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