map_castSuccEmb_uIcc — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem map_castSuccEmb_uIcc (i j : Fin n) : (uIcc i j).map castSuccEmb = uIcc i.castSucc j.castSucc :=
  map_castAddEmb_uIcc ..

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