finsetImage_castSucc_Icc — Mathlib

English

Let i,j ∈ Fin n. The image of Icc(i,j) under the successor-cast operation castSucc equals Icc(i.castSucc, j.castSucc).

Русский

Пусть i,j ∈ Fin n. Образ Icc(i,j) при отображении castSucc равен Icc(i.castSucc, j.castSucc).

LaTeX

$$$$ \operatorname{Finset.image}(\operatorname{castSucc}) (\operatorname{Finset.Icc}(i, j)) = \operatorname{Finset.Icc}(i.castSucc, j.castSucc) $$$$

Lean4

@[simp]
theorem finsetImage_castSucc_Icc (i j : Fin n) : (Icc i j).image castSucc = Icc i.castSucc j.castSucc :=
  finsetImage_castAdd_Icc ..

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