finsetImage_addNat_Ico — Mathlib

English

For Fin n, m, i, j in Fin n, the image of the half-open interval Ico i j under addNat m is the half-open interval Ico (i.addNat m) (j.addNat m).

Русский

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

LaTeX

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

Lean4

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

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