finsetImage_castSucc_Ioc — Mathlib

English

Let i,j ∈ Fin n. The image of Ioc(i,j) under castSucc equals Ioc i.castSucc j.castSucc.

Русский

Пусть i,j ∈ Fin n. Образ Ioc(i,j) при castSucc равен Ioc i.castSucc j.castSucc.

LaTeX

$$$$ \operatorname{Finset.image}(\operatorname{castSucc})(\operatorname{Finset.Ioc}(i, j)) = \operatorname{Finset.Ioc}(i.castSucc, j.castSucc) $$$$

Lean4

@[simp]
theorem finsetImage_castSucc_Ioc (i j : Fin n) : (Ioc i j).image castSucc = Ioc i.castSucc j.castSucc :=
  finsetImage_castAdd_Ioc ..

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