preimage_succ_uIoo_succ — Mathlib

English

Let i, j ∈ Fin(n). The preimage of the open-interval uIoo(i.succ, j.succ) under successor equals uIoo(i, j).

Русский

Пусть i, j ∈ Fin(n). Предобраз uIoo(i.succ, j.succ) по successor равен uIoo(i, j).

LaTeX

$$$\mathrm{Set.preimage}(\mathrm{Fin.succ}, \mathrm{Set.uIoo}(i.succ, j.succ)) = \mathrm{Set.uIoo}(i, j)$$$

Lean4

@[simp]
theorem preimage_succ_uIoo_succ (i j : Fin n) : succ ⁻¹' uIoo i.succ j.succ = uIoo i j :=
  preimage_addNat_uIoo_addNat ..

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