Gamma_strictMonoOn_Ici — Mathlib

English

Gamma is strictly increasing on the interval [2, ∞).

Русский

Гамма-функция строго возрастает на промежутке [2, ∞).

LaTeX

$$$ \text{StrictMonoOn}(\Gamma, [2, \infty)) $$$

Lean4

theorem Gamma_strictMonoOn_Ici : StrictMonoOn Gamma (Ici 2) :=
  by
  convert
    convexOn_Gamma.strict_mono_of_lt (by simp : (0 : ℝ) < 3 / 2) (by norm_num : (3 / 2 : ℝ) < 2)
      (Gamma_two.symm ▸ Gamma_three_div_two_lt_one)
  symm
  rw [inter_eq_right]
  exact fun x hx => two_pos.trans_le <| mem_Ici.mp hx

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