le_exp_of_log_le

Mathlib.Algebra.Order.GroupWithZero.Canonical

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

English

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

Русский

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

LaTeX

$$\log x \le a \Rightarrow x \le \exp a$$

Lean4

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

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

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

Разделы

Аффилиация

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