log_pos_of_isNNRat — Mathlib

English

If e is NNReal with NN representation as a NN rational, then log e > 0 under the given decidability condition.

Русский

Если e имеет представление как NNReal через NN-рационал, то log e > 0 при заданном условии решения.

LaTeX

$$$$ \\log e > 0. $$$$

Lean4

theorem log_pos_of_isNNRat {n : ℕ} : (NormNum.IsNNRat e n d) → (decide ((1 : ℚ) < n / d)) → (0 < Real.log (e : ℝ))
  | ⟨inv, eq⟩, h => by
    rw [eq, invOf_eq_inv, ← div_eq_mul_inv]
    have : 1 < (n : ℝ) / d := by simpa using (Rat.cast_lt (K := ℝ)).2 (of_decide_eq_true h)
    exact Real.log_pos this

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