preimage_castSucc_uIoc_castSucc — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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