monotoneOn_posLog — Mathlib

English

log⁺ is monotone on [0, ∞).

Русский

log⁺ монотонна на [0, ∞).

LaTeX

$$MonotoneOn( log^{+}, [0, \infty) )$$

Lean4

/-- The function `log⁺` is monotone on the positive axis. -/
theorem monotoneOn_posLog : MonotoneOn log⁺ (Set.Ici 0) :=
  by
  intro x hx y hy hxy
  simp only [posLog, le_sup_iff, sup_le_iff, le_refl, true_and]
  by_cases h : log x ≤ 0
  · tauto
  · right
    have := log_le_log (lt_trans Real.zero_lt_one ((log_pos_iff hx).1 (not_le.1 h))) hxy
    simp only [this, and_true, ge_iff_le]
    linarith

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