preimage_castSucc_Ico_castSucc — Mathlib

English

For any i, j ∈ Fin n, the preimage of Ico i.castSucc j.castSucc under castSucc equals Ico i j.

Русский

Для любых i, j ∈ Fin n, прообраз Ico i.castSucc j.castSucc под castSucc равен Ico i j.

LaTeX

$$$ \operatorname{Set.preimage}(\operatorname{Fin.castSucc})\, (\operatorname{Set.Ico} i.castSucc j.castSucc) = \operatorname{Ico} i j $$$

Lean4

@[simp]
theorem preimage_castSucc_Ico_castSucc (i j : Fin n) : castSucc ⁻¹' Ico i.castSucc j.castSucc = Ico i j :=
  rfl

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