strictMonoOn_logb_of_base_lt_one — Mathlib

English

Strictly monotone on the negative side: log_b is strictly increasing on (-∞, 0).

Русский

Строго монотонна на отрицательной половине: log_b строго возрастает на (-∞, 0).

LaTeX

$$StrictMonoOn (logb b) (Set.Iio 0)$$

Lean4

theorem strictMonoOn_logb_of_base_lt_one : StrictMonoOn (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_of_base_lt_one b_pos b_lt_one (abs_pos.2 hy.ne) ?_
  rwa [abs_of_neg hy, abs_of_neg hx, neg_lt_neg_iff]

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