preimage_castSucc_uIoo_castSucc — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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