m_pos

Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

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

English

Monotonicity of stepBound: if n ≤ m then stepBound(n) ≤ stepBound(m).

Русский

Монотонность stepBound: если n ≤ m, то stepBound(n) ≤ stepBound(m).

LaTeX

$$Monotone(SzemerediRegularity.stepBound)$$

Lean4

theorem m_pos [Nonempty α] (hPα : #P.parts * 16 ^ #P.parts ≤ card α) : 0 < m := by sz_positivity

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

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

Разделы

Аффилиация

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