seven_le_initialBound

Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

URI: https://scilib.ai/kg/mathlib#SzemerediRegularity.seven_le_initialBound

English

For all ε and l, 7 ≤ initialBound(ε, l).

Русский

Для всех ε и l верно 7 ≤ initialBound(ε, l).

LaTeX

$$$7 \le \mathrm{initialBound}(\varepsilon, l)$$$

Lean4

theorem seven_le_initialBound : 7 ≤ initialBound ε l :=
  le_max_left _ _

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

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

Разделы

Аффилиация

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