node4L_lemma₃

Mathlib.Data.Ordmap.Ordset

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

English

Let b, c, d be natural numbers with 2d ≤ b + c + 1 and b ≤ 3c. Then d ≤ 3c.

Русский

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

LaTeX

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

Lean4

theorem node4L_lemma₃ {b c d : ℕ} (mr₁ : 2 * d ≤ b + c + 1) (mm₁ : b ≤ 3 * c) : d ≤ 3 * c := by cutsat

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

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

Разделы

Аффилиация

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