clog_mono_right — Mathlib

English

If r1 > 0 and r1 ≤ r2, then clog_b(r1) ≤ clog_b(r2).

Русский

Если r1 > 0 и r1 ≤ r2, тогда clog_b(r1) ≤ clog_b(r2).

LaTeX

$$$0

Lean4

@[mono]
theorem clog_mono_right {b : ℕ} {r₁ r₂ : R} (h₀ : 0 < r₁) (h : r₁ ≤ r₂) : clog b r₁ ≤ clog b r₂ :=
  by
  have h₀' : 0 < r₂ := lt_of_lt_of_le h₀ h
  rw [← neg_log_inv_eq_clog, ← neg_log_inv_eq_clog, neg_le_neg_iff]
  exact log_mono_right (inv_pos_of_pos h₀') <| (inv_le_inv₀ h₀' h₀).2 h

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