succOrderEmb

Mathlib.Order.Fin.Basic

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

English

succOrderEmb (n) is an order-embedding from Fin n into Fin (n+1).

Русский

succOrderEmb(n) является вложением по порядку от Fin(n) к Fin(n+1).

LaTeX

$$$\mathrm{succOrderEmb}(n) : \mathrm{Fin}(n) \hookrightarrow^o \mathrm{Fin}(n+1)$$$

Lean4

/-- `Fin.succ` as an `OrderEmbedding` -/
def succOrderEmb (n : ℕ) : Fin n ↪o Fin (n + 1) :=
  .ofStrictMono succ strictMono_succ

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

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

Разделы

Аффилиация

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