add_one_le_two_mul

Mathlib.Algebra.Order.Ring.Unbundled.Basic

URI: https://scilib.ai/kg/mathlib#add_one_le_two_mul

← MathLib Explorer

English

For a ≥ 1 in a suitably ordered semiring, we have a + 1 ≤ 2a.

Русский

Пусть a ≥ 1 в порядковом полукольце; тогда a + 1 ≤ 2a.

LaTeX

$$$1 \le a \Rightarrow a + 1 \le 2a$$$

Lean4

theorem add_one_le_two_mul [LE R] [NonAssocSemiring R] [AddLeftMono R] {a : R} (a1 : 1 ≤ a) : a + 1 ≤ 2 * a :=
  calc
    a + 1 ≤ a + a := add_le_add_left a1 a
    _ = 2 * a := (two_mul _).symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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