image_natAdd_Ioc — Mathlib

English

Let m ∈ ℕ and i, j ∈ Fin(n). The image of the interval Ioc(i, j) under the translation by m is Ioc(i + m, j + m).

Русский

Пусть m ∈ ℕ и i, j ∈ Fin(n). Образ интервала Ioc(i, j) при сдвиге на m равен Ioc(i + m, j + m).

LaTeX

$$$$ \\mathrm{Set.image}(\\\\mathrm{Fin.natAdd}(m))(\\\\mathrm{Set.Ioc}(i,j)) = \\\\mathrm{Set.Ioc}(\\\\mathrm{Fin.natAdd}(m)i, \\\\mathrm{Fin.natAdd}(m)j). $$$$

Lean4

@[simp]
theorem image_natAdd_Ioc (m) (i j : Fin n) : natAdd m '' Ioc i j = Ioc (natAdd m i) (natAdd m j) :=
  by
  rw [← preimage_natAdd_Ioc_natAdd, image_preimage_eq_of_subset]
  exact Ioc_subset_Ioi_self.trans <| image_natAdd_Ioi m i ▸ image_subset_range _ _

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