lt_log_of_exp_lt — Mathlib

English

Let G be a preordered additive group and let exp: G → Gᵐ⁰ˣ and log: Gᵐ⁰ˣ → G denote the exponential and logarithm maps. If exp(a) < x for some x in Gᵐ⁰ˣ, then a < log(x).

Русский

Пусть G задана как упорядоченная аддитивная группа, и пусть экспонента exp: G → Gᵐ⁰ˣ и логарифм log: Gᵐ⁰ˣ → G задают экспоненциальное и логарифмическое отображения. Тогда если exp(a) < x для некоторого x ∈ Gᵐ⁰ˣ, то a < log(x).

LaTeX

$$$\exp(a) < x \quad\Rightarrow\quad a < \log x,$ для $a\in G$ и $x\in G^{\times}_{0}$.$$

Lean4

theorem lt_log_of_exp_lt (hax : exp a < x) : a < log x :=
  (lt_log_iff_exp_lt (exp_pos.trans hax).ne').2 hax

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