image_val_Icc — Mathlib

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

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