finsetImage_addNat_Icc — Mathlib

English

For Fin n, m, and i, j in Fin n, the image of the closed interval Icc i j under the map addNat m is the closed interval Icc (i.addNat m) (j.addNat m).

Русский

Для Fin n, m и i, j ∈ Fin n образ замкнутого интервала Icc i j под отображением addNat m равен замкнутому интервалу Icc (i.addNat m) (j.addNat m).

LaTeX

$$$ (Icc i j).image (addNat \cdot m) = Icc (i.addNat m) (j.addNat m) $$$

Lean4

@[simp]
theorem finsetImage_addNat_Icc (m) (i j : Fin n) : (Icc i j).image (addNat · m) = Icc (i.addNat m) (j.addNat m) := by
  simp [← coe_inj]

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