castLE_comp_castSucc — Mathlib

English

The composition Fin.castLE h ∘ Fin.castSucc equals Fin.castLE (Nat.le_of_succ_le h).

Русский

Состав Fin.castLE h ∘ Fin.castSucc равен Fin.castLE (Nat.le_of_succ_le h).

LaTeX

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

Lean4

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

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