image_castSucc_Ioi — Mathlib

English

The image of the interval Ioi i under the castSucc map is the interval Ioo i.castSucc (last n).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem image_castSucc_Ioi (i : Fin n) : castSucc '' Ioi i = Ioo i.castSucc (.last n) :=
  image_castAdd_Ioi ..

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