cast_inj

Mathlib.Data.Fin.SuccPred

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

English

For eq: n = m and a,b ∈ Fin n, a.cast eq = b.cast eq iff a = b.

Русский

Для eq: n = m и a,b ∈ Fin n: a.cast eq = b.cast eq эквивa a = b.

LaTeX

$$@[simp] $\\forall {n m : \\mathbb{N}} (eq : n = m) \\{a b : \\mathrm{Fin}(n)\\},\\; a.cast eq = b.cast eq \\iff a = b$$$

Lean4

@[simp]
theorem cast_inj (eq : n = m) {a b : Fin n} : a.cast eq = b.cast eq ↔ a = b := by simp [← val_inj]

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

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

Разделы

Аффилиация

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