exp_log — Mathlib

English

For all x,y, log x ≤ log y iff x ≤ y; equivalently, the order on ENNReal is transported by log.

Русский

Для любых x,y верно log x ≤ log y тогда и только тогда, когда x ≤ y; порядок переносится логарифмом.

LaTeX

$$$\\log x \\le \\log y \\iff x \\le y$$$

Lean4

@[simp]
theorem exp_log (x : ℝ≥0∞) : exp (log x) = x := by
  by_cases hx_top : x = ∞
  · simp [hx_top]
  by_cases hx_zero : x = 0
  · simp [hx_zero]
  have hx_pos : 0 < x.toReal := ENNReal.toReal_pos hx_zero hx_top
  rw [← ENNReal.ofReal_toReal hx_top, log_ofReal_of_pos hx_pos, exp_coe, Real.exp_log hx_pos]

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