castLE_castSucc

Mathlib.Data.Fin.SuccPred

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

English

For i ∈ Fin n and h, i.castSucc.castLE h = i.castLE (Nat.le_of_succ_le h).

Русский

Для i ∈ Fin(n) и h: i.castSucc.castLE h = i.castLE (Nat.le_of_succ_le h).

LaTeX

$$$\\forall {n m} (i : \\mathrm{Fin}(n)) (h : n + 1 \\le m),\\; i.castSucc.castLE h = i.castLE(\\mathrm{Nat}.le_of_succ_le\\; h)$$$

Lean4

@[simp]
theorem castLE_castSucc {n m} (i : Fin n) (h : n + 1 ≤ m) : i.castSucc.castLE h = i.castLE (Nat.le_of_succ_le h) :=
  rfl

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

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

Разделы

Аффилиация

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