hundred_le_m

Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

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

← MathLib Explorer

English

If a certain bound holds, then 100 ≤ m.

Русский

Если дано ограничение, то 100 ≤ m.

LaTeX

$$100 ≤ m$$

Lean4

theorem hundred_le_m [Nonempty α] (hPα : #P.parts * 16 ^ #P.parts ≤ card α) (hPε : 100 ≤ (4 : ℝ) ^ #P.parts * ε ^ 5)
    (hε : ε ≤ 1) : 100 ≤ m :=
  mod_cast
    (hundred_div_ε_pow_five_le_m hPα hPε).trans'
      (le_div_self (by simp) (by sz_positivity) <| pow_le_one₀ (by sz_positivity) hε)

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

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

Разделы

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

Аффилиация

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