valEmbedding

Mathlib.Data.Fin.Embedding

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

English

The natural inclusion map Fin(n) → ℕ is injective.

Русский

Естественное включение Fin(n) в ℕ инъективно.

LaTeX

$$Injective(\mathrm{val} : \mathrm{Fin}(n) \to \mathbb{N})$$

Lean4

/-- The inclusion map `Fin n → ℕ` is an embedding. -/
@[simps -fullyApplied apply]
def valEmbedding : Fin n ↪ ℕ :=
  ⟨val, val_injective⟩

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

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

Разделы

Аффилиация

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