half_lt_self

Mathlib.Data.NNReal.Defs

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

English

If a ≠ 0, then a/2 < a.

Русский

Если a ≠ 0, то a/2 < a.

LaTeX

$$$\forall a \in \mathbb{R}_{\ge 0},\ a \neq 0\Rightarrow \tfrac{a}{2} < a$$$

Lean4

nonrec theorem half_lt_self {a : ℝ≥0} (h : a ≠ 0) : a / 2 < a :=
  half_lt_self h.bot_lt

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

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

Разделы

Аффилиация

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