sinh_sub_id_strictMono — Mathlib

English

The function x ↦ sinh x − x is strictly increasing on ℝ.

Русский

Функция x ↦ sinh x − x строго возрастает на ℝ.

LaTeX

$$x

Lean4

theorem sinh_sub_id_strictMono : StrictMono fun x => sinh x - x :=
  by
  refine strictMono_of_odd_strictMonoOn_nonneg (fun x => by simp; abel) ?_
  refine strictMonoOn_of_deriv_pos (convex_Ici _) ?_ fun x hx => ?_
  · exact (continuous_sinh.sub continuous_id).continuousOn
  · rw [interior_Ici, mem_Ioi] at hx
    rw [deriv_fun_sub, deriv_sinh, deriv_id'', sub_pos, one_lt_cosh]
    exacts [hx.ne', differentiableAt_sinh, differentiableAt_id]

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