intervalIntegrable_inv_iff — Mathlib

English

The interval integrability of the function x^−1 on [a,b] is equivalent to a = b or 0 ∉ [a,b].

Русский

Интегрируемость по интервалу x^−1 на [a,b] эквивалентна a = b или 0 ∉ [a,b].

LaTeX

$$$\\text{IntervalIntegrable}(x^{-1}, \\text{volume}, a, b) \\iff a=b \\lor 0 \\notin [[a,b]]$$$

Lean4

/-- The function `fun x => x⁻¹` is integrable on `a..b` if and only if
`a = b` or `0 ∉ [a, b]`. -/
@[simp]
theorem intervalIntegrable_inv_iff {a b : ℝ} :
    IntervalIntegrable (fun x => x⁻¹) volume a b ↔ a = b ∨ (0 : ℝ) ∉ [[a, b]] := by
  simp only [← intervalIntegrable_sub_inv_iff, sub_zero]

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