logb_eq_iff_rpow_eq — Mathlib

English

A two-way equivalence: log_b y = x iff y = b^x, under suitable positivity constraints on b and y.

Русский

Двусторонняя эквивалентность: log_b y = x iff y = b^x при подходящих условиях на b и y.

LaTeX

$$$\log_b y = x \iff y = b^x \quad (b > 0, b \neq 1, y > 0)$$$

Lean4

theorem logb_eq_iff_rpow_eq (hy : 0 < y) : logb b y = x ↔ b ^ x = y :=
  by
  constructor <;> rintro rfl
  · exact rpow_logb b_pos b_ne_one hy
  · exact logb_rpow b_pos b_ne_one

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