lt_exp_of_log_lt

Mathlib.Algebra.Order.GroupWithZero.Canonical

URI: https://scilib.ai/kg/mathlib#WithZero.lt_exp_of_log_lt

English

If log x < a, then x < exp a.

Русский

Если log x < a, то x < exp a.

LaTeX

$$\log x < a \Rightarrow x < \exp a$$

Lean4

theorem lt_exp_of_log_lt (hxa : log x < a) : x < exp a := by
  obtain rfl | hx := eq_or_ne x 0 <;> simp [← log_lt_iff_lt_exp, *]

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

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

Разделы

Аффилиация

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