preimage_succ_uIcc_succ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem preimage_succ_uIcc_succ (i j : Fin n) : succ ⁻¹' uIcc i.succ j.succ = uIcc i j :=
  preimage_addNat_uIcc_addNat ..

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