merge_lemma

Mathlib.Data.Ordmap.Ordset

URI: https://scilib.ai/kg/mathlib#Ordnode.Valid'.merge_lemma

English

Let a, b, c be natural numbers. If 3a < b + c + 1 and b ≤ 3c, then 2(a + b) ≤ 9c + 5.

Русский

Пусть a, b, c — натуральные числа. Если 3a < b + c + 1 и b ≤ 3c, то 2(a + b) ≤ 9c + 5.

LaTeX

$$$\\forall a,b,c \\in \\mathbb{N},\\ (3a < b+c+1) \\land (b \\le 3c) \\Rightarrow 2(a+b) \\le 9c+5$$$

Lean4

theorem merge_lemma {a b c : ℕ} (h₁ : 3 * a < b + c + 1) (h₂ : b ≤ 3 * c) : 2 * (a + b) ≤ 9 * c + 5 := by cutsat

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

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

Разделы

Аффилиация

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