map_castSuccEmb_Ico — Mathlib

English

For i, j ∈ Fin n, mapping the half-open interval Ico i j via castSuccEmb gives Ico i.castSucc j.castSucc.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem map_castSuccEmb_Ico (i j : Fin n) : (Ico i j).map castSuccEmb = Ico i.castSucc j.castSucc :=
  map_castAddEmb_Ico ..

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