eulerMascheroniSeq_lt_eulerMascheroniConstant

English

For all m,n ∈ ℕ, eulerMascheroniSeq(m) < eulerMascheroniSeq'(n).

Русский

Для всех m,n ∈ ℕ выполняется eulerMascheroniSeq(m) < eulerMascheroniSeq'(n).

LaTeX

$$\forall m,n \in \mathbb{N},\ eulerMascheroniSeq(m) < eulerMascheroniSeq'(n)$$

Lean4

theorem eulerMascheroniSeq_lt_eulerMascheroniConstant (n : ℕ) : eulerMascheroniSeq n < eulerMascheroniConstant :=
  by
  refine (strictMono_eulerMascheroniSeq (Nat.lt_succ_self n)).trans_le ?_
  apply strictMono_eulerMascheroniSeq.monotone.ge_of_tendsto tendsto_eulerMascheroniSeq

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