map_natAddEmb_Ioi — Mathlib

English

Let n be a natural number, m a natural number, and i an element of Fin n. The image of the open-right interval Ioi i under the map natAddEmb m is exactly Ioi (natAdd m i).

Русский

Пусть n натурально, m натурально, и i ∈ Fin n. Образ открытого правого интервала Ioi i под отображением natAddEmb m совпадает с Ioi (natAdd m i).

LaTeX

$$$ (Ioi i).map (natAddEmb m) = Ioi (natAdd m i) $$$

Lean4

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

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