valOrderEmb

Mathlib.Order.Fin.Basic

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

English

The inclusion map Fin n → ℕ is an order embedding.

Русский

Включение Fin(n) в ℕ сохраняет порядок (является вложением по порядку).

LaTeX

$$$\mathrm{valOrderEmb}(n) : \mathrm{Fin}(n) \hookrightarrow^o \mathbb{N}$$$

Lean4

/-- The inclusion map `Fin n → ℕ` is an order embedding. -/
@[simps! apply]
def valOrderEmb (n) : Fin n ↪o ℕ :=
  ⟨valEmbedding, Iff.rfl⟩

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

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

Разделы

Аффилиация

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