finsetImage_natAdd_Ioo — Mathlib

English

For any natural m and i, j ∈ Fin n, image of Ioo i j under natAdd m equals Ioo (natAdd m i) (natAdd m j).

Русский

Для любого натурального m и i, j ∈ Fin n образ Ioo i j под natAdd m равен Ioo (natAdd m i) (natAdd m j).

LaTeX

$$$$(\\mathrm{Ioo}\\ i\\ j).\\operatorname{image}(\\mathrm{natAdd}\\ m) = \\mathrm{Ioo}(\\mathrm{natAdd}\\ m\,i, \\mathrm{natAdd}\\ m\,j)$$$$

Lean4

@[simp]
theorem finsetImage_natAdd_Ioo (m) (i j : Fin n) : (Ioo i j).image (natAdd m) = Ioo (natAdd m i) (natAdd m j) := by
  simp [← coe_inj]

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