castLE_inj

Mathlib.Data.Fin.SuccPred

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

English

For hmn: m ≤ n, a,b ∈ Fin m, castLE hmn a = castLE hmn b iff a = b.

Русский

Для hmn: m ≤ n, a,b ∈ Fin m, castLE hmn a = castLE hmn b тогда и только тогда a = b.

LaTeX

$$$\\forall {hmn : m \\le n},\\ a,b : \\mathrm{Fin}(m):\\; \\mathrm{castLE}\\ hmn\\ a = \\mathrm{castLE}\\ hmn\\ b \\iff a = b$$$

Lean4

@[simp]
theorem castLE_inj {hmn : m ≤ n} {a b : Fin m} : castLE hmn a = castLE hmn b ↔ a = b := by simp [Fin.ext_iff]

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

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

Разделы

Аффилиация

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