English
For i, j ∈ Fin n, the image of Icc(i, j) under Fin.val equals Icc(i, j).
Русский
Для i, j ∈ Fin(n) образ Icc(i, j) по Fin.val совпадает с Icc(i, j).
LaTeX
$$$$ \big(\operatorname{Fin.val}\big) '' \operatorname{Icc}(i, j) = \operatorname{Icc}(i, j). $$$$
Lean4
@[simp]
theorem image_val_Icc (i j : Fin n) : (↑) '' Icc i j = Icc (i : ℕ) j :=
by
rw [← preimage_val_Icc_val, image_preimage_eq_inter_range, range_val, inter_eq_left]
exact fun k hk ↦ hk.2.trans_lt j.is_lt