castAdd_inj

Mathlib.Data.Fin.SuccPred

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

English

For Fin m, castAdd n is injective: distinct a,b have distinct castAdd n values.

Русский

Для Fin m, castAdd n инъективен: различные a,b имеют различные значения castAdd n.

LaTeX

$$$\\forall {n m : \\mathbb{N}},\\; \\mathrm{Injective}(\\mathrm{Fin.castAdd}\\ n)$$$

Lean4

@[simp]
theorem castAdd_inj {a b : Fin m} : castAdd n a = castAdd n b ↔ a = b := by simp [Fin.ext_iff]

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

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

Разделы

Аффилиация

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