rotateL_lemma₁

Mathlib.Data.Ordmap.Ordset

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

English

For natural numbers a, b, c, if 3a ≤ b + c and c ≤ 3b, then a ≤ 3b.

Русский

Пусть a, b, c — натуральные числа и выполняются 3a ≤ b + c, c ≤ 3b. Тогда a ≤ 3b.

LaTeX

$$$ \forall a,b,c \in \mathbb{N},\ (3a \le b+c) \land (c \le 3b) \Rightarrow a \le 3b $$$

Lean4

theorem rotateL_lemma₁ {a b c : ℕ} (H2 : 3 * a ≤ b + c) (hb₂ : c ≤ 3 * b) : a ≤ 3 * b := by cutsat

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

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

Разделы

Аффилиация

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