image_castSucc_Iio — Mathlib

English

Let i be an element of Fin n. The image of the open interval Iio(i) under the castSucc map equals the open interval Iio(i.castSucc) in Fin(n+1).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem image_castSucc_Iio (i : Fin n) : castSucc '' Iio i = Iio i.castSucc :=
  image_castAdd_Iio ..

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