not_IntegrableOn_Ioi_inv — Mathlib

English

The inverse function is not interval integrable on any Ici-type interval.

Русский

Обратная функция не интегрируема на любом интервале типа Ici.

LaTeX

$$$\\neg \\text{IntervalIntegrable}(x^{-1}, \\text{volume}, a, b)$ where [a,b] is Ici-type$$

Lean4

/-- The function `fun x ↦ x⁻¹` is not integrable on any interval `(a, +∞)`. -/
theorem not_IntegrableOn_Ioi_inv {a : ℝ} : ¬IntegrableOn (·⁻¹) (Ioi a) := by
  simpa only [IntegrableOn, restrict_Ioi_eq_restrict_Ici] using not_IntegrableOn_Ici_inv

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