le_log_iff_exp_le

Mathlib.Algebra.Order.GroupWithZero.Canonical

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

English

For x ≠ 0, a ≤ log x iff exp a ≤ x.

Русский

Для x ≠ 0 верно: a ≤ log x эквивалентно exp a ≤ x.

LaTeX

$$(x \neq 0) \Rightarrow a \le \log x \iff \exp a \le x$$

Lean4

theorem le_log_iff_exp_le (hx : x ≠ 0) : a ≤ log x ↔ exp a ≤ x := by lift x to Multiplicative G using hx;
  simpa [log, exp] using .rfl

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

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

Разделы

Аффилиация

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