finsetImage_castSucc_Ioi — Mathlib

English

Let i be an element of Fin n. Then the image of the open right ray Ioi i under the map castSucc is the open interval Ioo i.castSucc (last n).

Русский

Пусть i — элемент Fin n. Тогда образ открытого правого полупрямоугольника Ioi i под отображением castSucc равен открытому интервалу Ioo i.castSucc (last n).

LaTeX

$$$$(\\mathrm{Ioi}\\ i).\\operatorname{image}(\\operatorname{castSucc}) = \\mathrm{Ioo}(i.castSucc, \\mathrm{last}\\ n)$$$$

Lean4

@[simp]
theorem finsetImage_castSucc_Ioi (i : Fin n) : (Ioi i).image castSucc = Ioo i.castSucc (.last n) :=
  finsetImage_castAdd_Ioi ..

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