box_succ_eq_sdiff — Mathlib

English

The next box equals the shell obtained by removing the inner interval: box(n+1) = Icc(-n.succ, n.succ) \ Icc(-n, n).

Русский

Следующая коробка равна оболочке, получаемой вычитанием внутреннего интервала: box(n+1) = Icc(-n.succ, n.succ) \ Icc(-n, n).

LaTeX

$$$\mathrm{box}(n+1) = \mathrm{Icc}(-n.succ, n.succ) \setminus \mathrm{Icc}(-n, n)$$$

Lean4

theorem box_succ_eq_sdiff (n : ℕ) : box (n + 1) = Icc (-n.succ : α) n.succ \ Icc (-n) n :=
  by
  rw [box, Icc_neg_mono.disjointed_add_one]
  simp only [Nat.cast_add_one, Nat.succ_eq_add_one]

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