log_neg

Mathlib.Analysis.SpecialFunctions.Log.Basic

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

English

If 0 < x < y then log x < log y.

Русский

Если 0 < x < y, то log x < log y.

LaTeX

$$$$ 0 < x < y \implies \log x < \log y. $$$$

Lean4

@[bound]
theorem log_neg (h0 : 0 < x) (h1 : x < 1) : log x < 0 :=
  (log_neg_iff h0).2 h1

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

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

Разделы

Аффилиация

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