preimage_addNat_Ico_addNat — Mathlib

English

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

Русский

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

LaTeX

$$$$ \\mathrm{Set.preimage}(\\\\mathrm{Fin.natAdd}(m))(\\\\mathrm{Set.Ico}(i.addNat m)(j.addNat m)) = \\\\mathrm{Set.Ico} i j. $$$$

Lean4

@[simp]
theorem preimage_addNat_Ico_addNat (m) (i j : Fin n) : (addNat · m) ⁻¹' Ico (i.addNat m) (j.addNat m) = Ico i j := by
  ext; simp

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