preimage_addNat_uIcc_addNat — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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