nValue_pos

Mathlib.Combinatorics.Additive.AP.Three.Behrend

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

English

If N ≥ 2, then nValue(N) > 0.

Русский

Если N ≥ 2, то nValue(N) > 0.

LaTeX

$$$$ 0 < nValue(N) \\quad\\text{for } N \\ge 2. $$$$

Lean4

theorem nValue_pos (hN : 2 ≤ N) : 0 < nValue N :=
  ceil_pos.2 <| Real.sqrt_pos.2 <| log_pos <| one_lt_cast.2 <| hN

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

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

Разделы

Аффилиация

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