image_castSucc_Ici — Mathlib

English

The image of the interval Ici i under the castSucc map is the interval Ico i.castSucc (last n).

Русский

Образ интервала Ici i при отображении castSucc равен интервалу Ico i.castSucc (последний элемент n).

LaTeX

$$$ \operatorname{image}(\operatorname{Fin.castSucc})\bigl(\operatorname{Ici} i\bigr) = \operatorname{Ico} i.castSucc (\operatorname{Fin.last} n) $$$

Lean4

@[simp]
theorem image_castSucc_Ici (i : Fin n) : castSucc '' Ici i = Ico i.castSucc (.last n) :=
  image_castAdd_Ici ..

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