one_half_lt_eulerMascheroniConstant

English

The sequence eulerMascheroniSeq' is strictly decreasing: for m < n, eulerMascheroniSeq'(m) > eulerMascheroniSeq'(n).

Русский

Последовательность eulerMascheroniSeq' строго убывает: если m < n, то eulerMascheroniSeq'(m) > eulerMascheroniSeq'(n).

LaTeX

$$\forall m eulerMascheroniSeq'(n)$$

Lean4

/-- Lower bound for `γ`. (The true value is about 0.57.) -/
theorem one_half_lt_eulerMascheroniConstant : 1 / 2 < eulerMascheroniConstant :=
  one_half_lt_eulerMascheroniSeq_six.trans (eulerMascheroniSeq_lt_eulerMascheroniConstant _)

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