neg_inv_le_log

Mathlib.Analysis.SpecialFunctions.Log.Basic

URI: https://scilib.ai/kg/mathlib#Real.neg_inv_le_log

← MathLib Explorer

English

For x ≥ 0, −x^{-1} ≤ log x.

Русский

Для x ≥ 0 верно −x^{-1} ≤ log x.

LaTeX

$$$x \\ge 0 \\\\Rightarrow -x^{-1} \\\\le \\\\log x$$$

Lean4

/-- See `Real.one_sub_inv_le_log_of_pos` for the stronger version when `x ≠ 0`. -/
theorem neg_inv_le_log (hx : 0 ≤ x) : -x⁻¹ ≤ log x := by rw [neg_le, ← log_inv]; exact log_le_self <| inv_nonneg.2 hx

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

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

Разделы

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

Аффилиация

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