log_le_iff_le_exp

Mathlib.Analysis.SpecialFunctions.Log.Basic

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

English

For x > 0, log x ≤ y iff x ≤ exp y.

Русский

Для x > 0 верно: log x ≤ y тогда и только тогда, когда x ≤ exp y.

LaTeX

$$$$ \log x \le y \iff x \le \exp y \quad (x>0). $$$$

Lean4

theorem log_le_iff_le_exp (hx : 0 < x) : log x ≤ y ↔ x ≤ exp y := by rw [← exp_le_exp, exp_log hx]

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

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

Разделы

Аффилиация

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