map_succEmb_uIcc — Mathlib

English

Let i, j ∈ Fin n. Then the image of the unified interval uIcc(i, j) under succEmb n is uIcc(i.succ, j.succ).

Русский

Пусть i, j ∈ Fin n. Тогда образ объединённого интервала uIcc(i, j) под succEmb n равен uIcc(i.succ, j.succ).

LaTeX

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

Lean4

@[simp]
theorem map_succEmb_uIcc (i j : Fin n) : (uIcc i j).map (succEmb n) = uIcc i.succ j.succ :=
  map_addNatEmb_uIcc ..

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