le_stepBound

Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

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

English

StepBound is monotone: if n ≤ m, then stepBound(n) ≤ stepBound(m).

Русский

StepBound монотонна: если n ≤ m, то stepBound(n) ≤ stepBound(m).

LaTeX

$$$n \le m \Rightarrow \mathrm{stepBound}(n) \le \mathrm{stepBound}(m).$$$

Lean4

theorem le_stepBound : id ≤ stepBound := fun n => Nat.le_mul_of_pos_right _ <| pow_pos (by simp) n

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

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

Разделы

Аффилиация

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