English
Let i and j be elements of Fin(n). Then the image of the half-open interval Ioc(i, j) under the natural embedding Fin(n) → N equals the half-open interval Ioc(i, j) in the natural numbers, i.e. the set {k ∈ N : i < k ≤ j} is precisely the image of {k ∈ Fin(n) : i < k ≤ j} under the inclusion.
Русский
Пусть i и j — элементы Fin(n). Тогда образ полуоткрытого интервала Ioc(i, j) в N под естественным вложением Fin(n) → N равен интервалу Ioc(i, j) в натуральных числах; то есть множество {k ∈ N : i < k ≤ j} совпадает с образом множества {k ∈ Fin(n) : i < k ≤ j} при включении.
LaTeX
$$$(\uparrow) '' \mathrm{Ioc}(i, j) = \mathrm{Ioc}(i, j) \quad\text{for } i,j \in \mathrm{Fin}(n)$$$
Lean4
@[simp]
theorem image_val_Ioc (i j : Fin n) : (↑) '' Ioc i j = Ioc (i : ℕ) j :=
by
rw [← preimage_val_Ioc_val, image_preimage_eq_inter_range, range_val, inter_eq_left]
exact fun k hk ↦ hk.2.trans_lt j.is_lt
