half_lt_self

Mathlib.Data.ENNReal.Inv

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

← MathLib Explorer

English

If a ≠ ∞ and a ≠ 0, then a/2 < a in ENNReal.

Русский

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

LaTeX

$$$$ \forall a, a \neq 0 \land a \neq \infty \Rightarrow a/2 < a. $$$$

Lean4

protected theorem half_lt_self (hz : a ≠ 0) (ht : a ≠ ∞) : a / 2 < a :=
  by
  lift a to ℝ≥0 using ht
  rw [coe_ne_zero] at hz
  rw [← coe_two, ← coe_div, coe_lt_coe]
  exacts [NNReal.half_lt_self hz, two_ne_zero' _]

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

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

Разделы

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

Аффилиация

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