lower_bound_le_one

Mathlib.Combinatorics.Additive.AP.Three.Behrend

URI: https://scilib.ai/kg/mathlib#Behrend.lower_bound_le_one

← MathLib Explorer

English

If N ≥ 64, then 3 ≤ nValue(N).

Русский

Если N ≥ 64, то 3 ≤ nValue(N).

LaTeX

$$$$ N \\ge 64 \\Rightarrow 3 \\le nValue(N). $$$$

Lean4

theorem lower_bound_le_one (hN : 1 ≤ N) (hN' : N ≤ 4096) : (N : ℝ) * exp (-4 * √(log N)) ≤ 1 :=
  by
  obtain rfl | hN := hN.eq_or_lt
  · simp
  · exact lower_bound_le_one' hN hN'

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

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

Разделы

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

Аффилиация

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