mul_log_eq_log_iff — Mathlib

English

Let x > 0 and z > 0. Then y log x = log z iff x^y = z.

Русский

Пусть x > 0 и z > 0. Тогда y log x = log z если и только если x^y = z.

LaTeX

$$$\\\\forall x > 0, \\\\forall z > 0: \\\\bigl(y \\\\log x = \\log z \\\\bigr) \iff x^y = z.$$$

Lean4

theorem mul_log_eq_log_iff {x y z : ℝ} (hx : 0 < x) (hz : 0 < z) : y * log x = log z ↔ x ^ y = z :=
  ⟨fun h ↦ log_injOn_pos (rpow_pos_of_pos hx _) hz <| log_rpow hx _ |>.trans h, by rintro rfl; rw [log_rpow hx]⟩

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