strictAntiOn_logb — Mathlib

English

The function log_b is strictly anti-monotone on the negative reals: if x < y < 0 then log_b x > log_b y.

Русский

Функция log_b строго убывает на отрицательных числах: если x < y < 0, то log_b x > log_b y.

LaTeX

$$$1 < b \Rightarrow \text{StrictAntiOn}(\log_b, \mathbb{R}_{<0}).$$$

Lean4

theorem strictAntiOn_logb : StrictAntiOn (logb b) (Set.Iio 0) :=
  by
  rintro x (hx : x < 0) y (hy : y < 0) hxy
  rw [← logb_abs b y, ← logb_abs b x]
  refine logb_lt_logb hb (abs_pos.2 hy.ne) ?_
  rwa [abs_of_neg hy, abs_of_neg hx, neg_lt_neg_iff]

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