finsetImage_castSucc_Iio — Mathlib

English

Let i ∈ Fin n. The image of the left-open interval Iio i under castSuccEmb is Iio i.castSucc.

Русский

Пусть i ∈ Fin n. Образ левостороннего открытого интервала Iio i под castSuccEmb равен Iio i.castSucc.

LaTeX

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

Lean4

@[simp]
theorem finsetImage_castSucc_Iio (i : Fin n) : (Iio i).image castSucc = Iio i.castSucc :=
  finsetImage_castAdd_Iio ..

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