map_natAddEmb_uIcc — Mathlib

English

For m ∈ Nat, i, j ∈ Fin n, map (natAddEmb m) on uIcc i j equals uIcc (natAdd m i) (natAdd m j).

Русский

Для m ∈ Nat, i, j ∈ Fin n отображение natAddEmb m на uIcc i j даёт uIcc (natAdd m i) (natAdd m j).

LaTeX

$$$$(\\mathrm{Finset.map}\\;\\mathrm{natAddEmb}\\ m)\\ (\\mathrm{uIcc}\\ i\\ j) = \\mathrm{uIcc}(\\mathrm{natAdd}\\ m\,i, \\mathrm{natAdd}\\ m\,j)$$$$

Lean4

@[simp]
theorem map_natAddEmb_uIcc (m) (i j : Fin n) : (uIcc i j).map (natAddEmb m) = uIcc (natAdd m i) (natAdd m j) := by
  simp [← coe_inj]

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