image_succ_Iic — Mathlib

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

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