mono

Mathlib.Combinatorics.Additive.AP.Three.Defs

URI: https://scilib.ai/kg/mathlib#ThreeGPFree.mono

English

For all N, rothNumberNat N is at least (N)·exp(−4√(ln N)).

Русский

Для всех N rothNumberNat N не меньше N e^{−4√(ln N)}.

LaTeX

$$$$ rothNumberNat N \\ge N \\cdot \\exp(-4 \\sqrt{\\log N}) . $$$$

Lean4

@[to_additive]
theorem mono (h : t ⊆ s) (hs : ThreeGPFree s) : ThreeGPFree t := fun _ ha _ hb _ hc ↦ hs (h ha) (h hb) (h hc)

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

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

Разделы

Аффилиация

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