half_le_self

Mathlib.Data.NNReal.Defs

URI: https://scilib.ai/kg/mathlib#NNReal.half_le_self

English

For any a in ℝ≥0, a/2 ≤ a.

Русский

Для любого a ∈ ℝ≥0 верно a/2 ≤ a.

LaTeX

$$$\forall a \in \mathbb{R}_{\ge 0},\ \tfrac{a}{2} \le a$$$

Lean4

nonrec theorem half_le_self (a : ℝ≥0) : a / 2 ≤ a :=
  half_le_self bot_le

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

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

Разделы

Аффилиация

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