eulerMascheroniConstant_lt_eulerMascheroniSeq'

English

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

Русский

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

LaTeX

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

Lean4

theorem eulerMascheroniConstant_lt_eulerMascheroniSeq' (n : ℕ) : eulerMascheroniConstant < eulerMascheroniSeq' n :=
  by
  refine lt_of_le_of_lt ?_ (strictAnti_eulerMascheroniSeq' (Nat.lt_succ_self n))
  apply strictAnti_eulerMascheroniSeq'.antitone.le_of_tendsto tendsto_eulerMascheroniSeq'

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