coe_castPred

Mathlib.Data.Fin.SuccPred

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

English

The natural-number value of castPred(i,h) equals i.

Русский

Натуральное значение castPred(i,h) равно i.

LaTeX

$$$$ \\@[simp] \\forall {n}, (i : \\mathrm{Fin}(n+1)) (h): (\\operatorname{castPred}(i,h) : \\mathbb{N}) = i. $$$$

Lean4

@[simp]
theorem coe_castPred (i : Fin (n + 1)) (h : i ≠ last _) : (castPred i h : ℕ) = i :=
  rfl

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

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

Разделы

Аффилиация

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