half_le_self

Mathlib.Data.ENNReal.Inv

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

English

For any a ∈ ENNReal, a/2 ≤ a.

Русский

Для любого a ∈ ENNReal, a/2 ≤ a.

LaTeX

$$$$ a/2 \le a. $$$$

Lean4

protected theorem half_le_self : a / 2 ≤ a :=
  le_add_self.trans_eq <| ENNReal.add_halves _

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

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

Разделы

Аффилиация

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