English
The image of the closed-down interval Iic(i) under succ equals the open interval Ioc 0 i.succ.
Русский
Образ Iic(i) под succ есть Ioc 0 i.succ.
LaTeX
$$$\mathrm{Set.image}(\mathrm{Fin.succ}, \mathrm{Set.Iic}(i)) = \mathrm{Set.Ioc}(0, i.succ)$$$
Lean4
@[simp]
theorem image_succ_Iic (i : Fin n) : succ '' Iic i = Ioc 0 i.succ :=
by
refine Subset.antisymm (image_subset_iff.mpr fun j hj ↦ ⟨j.succ_pos, succ_le_succ_iff.2 hj⟩) ?_
rintro j ⟨hj₀, hj⟩
rcases exists_succ_eq_of_ne_zero hj₀.ne' with ⟨j, rfl⟩
exact mem_image_of_mem _ <| succ_le_succ_iff.mp hj