log_monotone — Mathlib

English

For any base b, the function y ↦ log_b y is nondecreasing.

Русский

Для любого основания b функция y ↦ log_b y неубывающая.

LaTeX

$$$\\forall b \\in \\mathbb{N}, \\; \\text{Monotone}(\\log_b) \\text{ i.e. } \\; \\forall y_1,y_2 \\in \\mathbb{N}, y_1 \\le y_2 \\Rightarrow \\log_b y_1 \\le \\log_b y_2$$$

Lean4

theorem log_monotone {b : ℕ} : Monotone (log b) :=
  by
  refine monotone_nat_of_le_succ fun n => ?_
  rcases le_or_gt b 1 with hb | hb
  · rw [log_of_left_le_one hb]
    exact zero_le _
  · exact le_log_of_pow_le hb (pow_log_le_add_one _ _)

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