box_succ_union_prod

Mathlib.Order.Interval.Finset.Box

URI: https://scilib.ai/kg/mathlib#Finset.box_succ_union_prod

English

The union of box(n+1) and Icc(-n,n) equals Icc(-n.succ, n.succ).

Русский

Объединение box(n+1) и Icc(-n,n) даёт Icc(-n.succ, n.succ).

LaTeX

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

Lean4

@[simp]
theorem box_succ_union_prod (n : ℕ) : box (n + 1) ∪ Icc (-n : α) n = Icc (-n.succ : α) n.succ :=
  Icc_neg_mono.disjointed_add_one_sup _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru