initialBound_le_bound

Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

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

← MathLib Explorer

English

initialBound(ε, l) ≤ bound(ε, l).

Русский

initialBound(ε, l) ≤ bound(ε, l).

LaTeX

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

Lean4

theorem initialBound_le_bound : initialBound ε l ≤ bound ε l :=
  (id_le_iterate_of_id_le le_stepBound _ _).trans <| Nat.le_mul_of_pos_right _ <| by positivity

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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