image_succ_uIoo — Mathlib

English

The image of the set uIoo under the successor map equals the shifted interval: succ''uIoo i j = uIoo i.succ j.succ.

Русский

Образ множества uIoo под переходом к следующему элементу равен смещённому интервалу: succ''uIoo i j = uIoo i.succ j.succ.

LaTeX

$$$ \text{succ} '' \text{uIoo}(i,j) = \text{uIoo}(i.succ, j.succ) $$$

Lean4

@[simp]
theorem image_succ_uIoo (i j : Fin n) : succ '' uIoo i j = uIoo i.succ j.succ :=
  image_addNat_uIoo ..

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