map_castSuccEmb_Icc — Mathlib

English

For i, j ∈ Fin n, mapping the closed interval Icc i j through castSuccEmb yields Icc i.castSucc j.castSucc.

Русский

Для i, j ∈ Fin n отображение castSuccEmb переводит закрытый интервал Icc i j в Icc i.castSucc j.castSucc.

LaTeX

$$$$(\\mathrm{Finset.map}\\;\\operatorname{castSuccEmb})\\ (\\mathrm{Icc}\\ i\\ j) = \\mathrm{Icc}(i.castSucc, j.castSucc)$$$$

Lean4

@[simp]
theorem map_castSuccEmb_Icc (i j : Fin n) : (Icc i j).map castSuccEmb = Icc i.castSucc j.castSucc :=
  map_castAddEmb_Icc ..

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