log_pos_iff

Mathlib.Analysis.SpecialFunctions.Log.Basic

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

← MathLib Explorer

English

For x > 0, log x > 0 iff x > 1.

Русский

Для x > 0 log x > 0 тогда и только тогда, когда x > 1.

LaTeX

$$$$ 0 < \log x \iff 1 < x \quad (x>0). $$$$

Lean4

theorem log_pos_iff (hx : 0 ≤ x) : 0 < log x ↔ 1 < x :=
  by
  rcases hx.eq_or_lt with (rfl | hx)
  · simp [zero_le_one]
  rw [← log_one]
  exact log_lt_log_iff zero_lt_one hx

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

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

Разделы

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

Аффилиация

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