map_succEmb_Ico — Mathlib

English

Let i, j ∈ Fin n. Then the image of the finite interval Ico(i, j) under the successor-embedding map equals the interval Ico(i.succ, j.succ).

Русский

Пусть i, j ∈ Fin n. Тогда образ конечного интервала Ico(i, j) под отображением succEmb n равен интервалу Ico(i.succ, j.succ).

LaTeX

$$$ (Ico i j).map (succEmb n) = Ico i.succ j.succ $$$

Lean4

@[simp]
theorem map_succEmb_Ico (i j : Fin n) : (Ico i j).map (succEmb n) = Ico i.succ j.succ :=
  map_addNatEmb_Ico ..

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