log_nonpos_iff

Mathlib.Analysis.SpecialFunctions.Log.Basic

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

← MathLib Explorer

English

For x ≥ 0, log x ≤ 0 iff x ≤ 1.

Русский

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

LaTeX

$$$$ \log x \le 0 \iff x \le 1 \quad (x \ge 0). $$$$

Lean4

theorem log_nonpos_iff (hx : 0 ≤ x) : log x ≤ 0 ↔ x ≤ 1 :=
  by
  rcases hx.eq_or_lt with (rfl | hx)
  · simp [le_refl, zero_le_one]
  rw [← not_lt, log_pos_iff hx.le, not_lt]

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

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

Разделы

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

Аффилиация

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