image_val_Ico — Mathlib

English

For i, j ∈ Fin n, the image of Ico(i, j) under Fin.val equals Ico(i, j).

Русский

Для i, j ∈ Fin(n) образ Ico(i, j) по Fin.val совпадает с Ico(i, j).

LaTeX

$$$$ \big(\operatorname{Fin.val}\big) '' \operatorname{Ico}(i, j) = \operatorname{Ico}(i, j). $$$$

Lean4

@[simp]
theorem image_val_Ico (i j : Fin n) : (↑) '' Ico i j = Ico (i : ℕ) j :=
  by
  rw [← preimage_val_Ico_val, image_preimage_eq_inter_range, range_val, inter_eq_left]
  exact fun k hk ↦ hk.2.trans j.is_lt

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