log_nonneg_of_isNegNat — Mathlib

English

If e is the negative of a natural number, then log e > 0 (interpreting via appropriate transformations; positivity of log under the given numeric interpretation).

Русский

Если e есть отрицательное целое, образованное как минус натурального числа, то log e > 0 (в рамках соответствующей интерпретации числовых функций).

LaTeX

$$$$ \\text{If } e = -n, \\ n\\ge 1, \\log(e) > 0. $$$$

Lean4

theorem log_nonneg_of_isNegNat {n : ℕ} (h : NormNum.IsInt e (.negOfNat n)) : 0 ≤ Real.log (e : ℝ) :=
  by
  rw [NormNum.IsInt.neg_to_eq h rfl]
  exact Real.log_neg_natCast_nonneg _

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