preimage_addNat_uIoo_addNat — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem preimage_addNat_uIoo_addNat (m) (i j : Fin n) : (addNat · m) ⁻¹' uIoo (i.addNat m) (j.addNat m) = uIoo i j := by
  simp [uIoo, ← (strictMono_addNat m).monotone.map_max, ← (strictMono_addNat m).monotone.map_min]

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