map_castSuccEmb_Ioc — Mathlib

English

For i, j ∈ Fin n, mapping the half-open interval Ioc i j through castSuccEmb yields Ioc i.castSucc j.castSucc.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem map_castSuccEmb_Ioc (i j : Fin n) : (Ioc i j).map castSuccEmb = Ioc i.castSucc j.castSucc :=
  map_castAddEmb_Ioc ..

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