node4L_lemma₁ — Mathlib

English

A numerical inequality lemma used in balancing a four-node left configuration; under certain inequalities, a bound on b is strictly less than 3a+1.

Русский

Лемма неравенств в четырехузловой конфигурации слева; при выполнении некоторых неравенств, b строго меньше 3a+1.

LaTeX

$$$\\forall a,b,c,d \\in \\mathbb{N},\\; lr_2: 3*(b+c+1+d) \\le 16*a + 9 \\wedge mr_2: b+c+1 \\le 3*d \\wedge mm_1: b \\le 3*c \\Rightarrow b < 3*a + 1.$$$

Lean4

theorem node4L_lemma₁ {a b c d : ℕ} (lr₂ : 3 * (b + c + 1 + d) ≤ 16 * a + 9) (mr₂ : b + c + 1 ≤ 3 * d)
    (mm₁ : b ≤ 3 * c) : b < 3 * a + 1 := by cutsat

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