le_bound

Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

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

English

l ≤ bound(ε, l).

Русский

l ≤ bound(ε, l).

LaTeX

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

Lean4

theorem le_bound : l ≤ bound ε l :=
  (le_initialBound ε l).trans <| initialBound_le_bound ε l

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

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

Разделы

Аффилиация

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