eulerMascheroniSeq_lt_eulerMascheroniSeq'

English

For all m,n in natural numbers, 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_eulerMascheroniSeq' (m n : ℕ) : eulerMascheroniSeq m < eulerMascheroniSeq' n :=
  by
  have (r : ℕ) : eulerMascheroniSeq r < eulerMascheroniSeq' r :=
    by
    rcases eq_zero_or_pos r with rfl | hr
    · simp [eulerMascheroniSeq, eulerMascheroniSeq']
    simp only [eulerMascheroniSeq, eulerMascheroniSeq', hr.ne', if_false]
    gcongr
    linarith
  apply (strictMono_eulerMascheroniSeq.monotone (le_max_left m n)).trans_lt
  exact (this _).trans_le (strictAnti_eulerMascheroniSeq'.antitone (le_max_right m n))

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