mem_box

Mathlib.Combinatorics.Additive.AP.Three.Behrend

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

English

An element x ∈ Fin n → Nat lies in box n d iff for every coordinate i, x(i) < d.

Русский

Элемент x ∈ Fin n → Nat принадлежит box n d тогда и только тогда, когда для каждой координаты i выполняется x(i) < d.

LaTeX

$$$$ x \in \mathrm{box}(n,d) \iff \forall i, x(i) < d $$$$

Lean4

theorem mem_box : x ∈ box n d ↔ ∀ i, x i < d := by simp only [box, Fintype.mem_piFinset, mem_range]

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

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

Разделы

Аффилиация

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