rpow_logb_of_neg — Mathlib

English

If x < 0 and base conditions hold, then b^{log_b x} equals |x| with a sign-related adjustment.

Русский

Если x < 0 и соблюдаются условия основания, то b^{log_b x} относится к |x| с учетом знака.

LaTeX

$$$b^{\log_b x} = |x| \quad (x < 0, \\text{conditions on } b)$$$

Lean4

theorem rpow_logb_of_neg (hx : x < 0) : b ^ logb b x = -x :=
  by
  rw [rpow_logb_eq_abs b_pos b_ne_one (ne_of_lt hx)]
  exact abs_of_neg hx

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