finsetImage_cast_Icc — Mathlib

English

Let h be a equality n = m and i,j ∈ Fin n. The image of the closed interval Icc(i,j) under Fin.cast h is exactly the closed interval Icc(i.cast h, j.cast h).

Русский

Пусть h : n = m и i, j ∈ Fin n. Образ замкнутого отрезка Icc(i,j) при приводлении Fin.cast h равен замкнутому отрезку Icc(i.cast h, j.cast h).

LaTeX

$$$$ \operatorname{Finset.image}(\operatorname{Fin.cast} h)(\operatorname{Finset.Icc}(i, j)) = \operatorname{Finset.Icc}(\operatorname{Fin.cast} h\, i) (\operatorname{Fin.cast} h\, j) $$$$

Lean4

@[simp]
theorem finsetImage_cast_Icc (h : n = m) (i j : Fin n) : (Icc i j).image (.cast h) = Icc (i.cast h) (j.cast h) := by
  simp [← coe_inj]

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