box_zero

Mathlib.Combinatorics.Additive.AP.Three.Behrend

URI: https://scilib.ai/kg/mathlib#Behrend.box_zero

English

Box with width zero is empty when d = 0, i.e., box(n+1,0) = ∅.

Русский

Ящик с размером 0 пуст; box(n+1,0) = ∅.

LaTeX

$$$$ \mathrm{box}(n+1,0) = \emptyset $$$$

Lean4

@[simp]
theorem box_zero : box (n + 1) 0 = ∅ := by simp [box]

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

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

Разделы

Аффилиация

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