eps_pow_five_pos

Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

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

← MathLib Explorer

English

One ≤ m in a real-coercion sense under a bound.

Русский

Единица не превосходит m после канонического отображения в вещественные.

LaTeX

$$1 ≤ m$$

Lean4

theorem eps_pow_five_pos (hPε : 100 ≤ (4 : ℝ) ^ #P.parts * ε ^ 5) : ↑0 < ε ^ 5 :=
  pos_of_mul_pos_right ((by simp : (0 : ℝ) < 100).trans_le hPε) <| by positivity

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

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

Разделы

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

Аффилиация

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