log_pos_of_isNat — Mathlib

English

If e is a natural number (represented as a real), then log e ≥ 0 (since e ≥ 1 for e ≠ 0).

Русский

Если e является натуральным числом, представленным как вещественное, то log e ≥ 0 (так как e ≥ 1 при e ≠ 0).

LaTeX

$$$$ \\log e \\ge 0 \\quad \\text{for } e = n \\in \\mathbb{N} \\subset \\mathbb{R}. $$$$

Lean4

theorem log_pos_of_isNat {n : ℕ} (h : NormNum.IsNat e n) (w : Nat.blt 1 n = true) : 0 < Real.log (e : ℝ) :=
  by
  rw [NormNum.IsNat.to_eq h rfl]
  apply Real.log_pos
  simpa using w

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