log_lt_iff_lt_exp

Mathlib.Analysis.SpecialFunctions.Log.Basic

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

English

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

Русский

Для x > 0: log x < y тогда и только тогда, когда x < exp y.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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