le_log_iff_exp_le

Mathlib.Analysis.SpecialFunctions.Log.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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