integral_one_div — Mathlib

English

If 0 is not in the closed interval [a,b], then ∫_a^b 1/x dx = log(b/a).

Русский

Если 0 не принадлежит замкнутому интервалу [a,b], то ∫_a^b 1/x dx = log(b/a).

LaTeX

$$$\forall a,b \in \mathbb{R},\ 0 \notin [a,b] \Rightarrow \displaystyle \int_a^b \frac{1}{x} \, dx = \log\left( \frac{b}{a} \right)$$$

Lean4

theorem integral_one_div (h : (0 : ℝ) ∉ [[a, b]]) : ∫ x : ℝ in a..b, 1 / x = log (b / a) := by
  simp only [one_div, integral_inv h]

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