one_sub_inv_le_log_of_pos

Mathlib.Analysis.SpecialFunctions.Log.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

theorem one_sub_inv_le_log_of_pos (hx : 0 < x) : 1 - x⁻¹ ≤ log x := by
  simpa [add_comm] using log_le_sub_one_of_pos (inv_pos.2 hx)

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

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

Разделы

Аффилиация

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