image_castSucc_Icc — Mathlib

English

Let i and j be elements of Fin n. The image of the closed interval Icc(i, j) under castSucc is the closed interval Icc(i.castSucc, j.castSucc) in Fin(n+1).

Русский

Пусть i и j ∈ Fin n. Образ замкнутого интервала Icc(i, j) под castSucc равен замкнутому интервалу Icc(i.castSucc, j.castSucc) в Fin(n+1).

LaTeX

$$$\operatorname{Set.image}(\mathrm{Fin.castSucc}, \mathrm{Set.Icc}(i, j)) = \mathrm{Set.Icc}(i.castSucc, j.castSucc)$$$

Lean4

@[simp]
theorem image_castSucc_Icc (i j : Fin n) : castSucc '' Icc i j = Icc i.castSucc j.castSucc :=
  image_castAdd_Icc ..

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