finsetImage_castSucc_uIcc — Mathlib

English

Let i,j ∈ Fin n. The image of uIcc(i,j) under castSucc equals uIcc i.castSucc j.castSucc.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem finsetImage_castSucc_uIcc (i j : Fin n) : (uIcc i j).image castSucc = uIcc i.castSucc j.castSucc :=
  finsetImage_castAdd_uIcc ..

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