image_addNat_Ioo — Mathlib

English

For all m ∈ ℕ and i, j ∈ Fin(n), the image of Ioo i j under x ↦ x + m is Ioo(i + m, j + m).

Русский

Для всех m ∈ ℕ и i, j ∈ Fin(n) образ Ioo i j при сдвиге на m равен Ioo(i + m, j + m).

LaTeX

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

Lean4

@[simp]
theorem image_addNat_Ioo (m) (i j : Fin n) : (addNat · m) '' Ioo i j = Ioo (i.addNat m) (j.addNat m) :=
  by
  rw [← preimage_addNat_Ioo_addNat, image_preimage_eq_of_subset]
  exact Ioo_subset_Ioi_self.trans <| image_addNat_Ioi m i ▸ image_subset_range _ _

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