preimage_addNat_uIoc_addNat — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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