finsetImage_castSucc_Iic — Mathlib

English

Let i be in Fin n. The image of the left-closed interval Iic i under castSucc is Iic i.castSucc.

Русский

Пусть i ∈ Fin n. Образ лево-ограниченного интервала Iic i под castSucc равен Iic i.castSucc.

LaTeX

$$$$(\\mathrm{Iic}\\ i).\\operatorname{image}(\\operatorname{castSucc}) = \\mathrm{Iic}(i.castSucc)$$$$

Lean4

@[simp]
theorem finsetImage_castSucc_Iic (i : Fin n) : (Iic i).image castSucc = Iic i.castSucc :=
  finsetImage_castAdd_Iic ..

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