map_natAddEmb_Ioc — Mathlib

English

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

Русский

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

LaTeX

$$$$(\\mathrm{Ioo}\\ i\\ j).\\operatorname{map}(\\mathrm{natAddEmb}\\ m) = \\mathrm{Ioo}(\\mathrm{natAdd}\\ m\,i, \\mathrm{natAdd}\\ m\,j)$$$$

Lean4

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

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