le_initialBound

Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

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

English

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

Русский

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

LaTeX

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

Lean4

theorem le_initialBound : l ≤ initialBound ε l :=
  (le_max_left _ _).trans <| le_max_right _ _

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

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

Разделы

Аффилиация

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