stepBound_mono

Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

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

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 stepBound_mono : Monotone stepBound := fun _ _ h => by unfold stepBound; gcongr; decide

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

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

Разделы

Аффилиация

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