initialBound_pos

Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

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

English

The initial bound is strictly positive for all ε and l.

Русский

Начальная граница положительна для всех ε и l.

LaTeX

$$$0 < \mathrm{initialBound}(\varepsilon, l)$$$

Lean4

theorem initialBound_pos : 0 < initialBound ε l :=
  Nat.succ_pos'.trans_le <| seven_le_initialBound _ _

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

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

Разделы

Аффилиация

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