image_succ_Iio — Mathlib

English

The image of the open-interval Iio(i) under succ equals the open-interval Ioo 0 i.succ.

Русский

Образ Iio(i) под succ равен Ioo 0 i.succ.

LaTeX

$$$\mathrm{Set.image}(\mathrm{Fin.succ}, \mathrm{Set.Iio}(i)) = \mathrm{Set.Ioo}(0, i.succ)$$$

Lean4

@[simp]
theorem image_succ_Iio (i : Fin n) : succ '' Iio i = Ioo 0 i.succ :=
  by
  refine Subset.antisymm (image_subset_iff.mpr fun j hj ↦ ⟨j.succ_pos, succ_lt_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_lt_succ_iff.mp hj

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