intervalIntegrable_one_div — Mathlib

English

Under mild hypotheses, the reciprocal function on an interval is interval-integrable.

Русский

При умеренных условиях обратная функция на интервале интегрируема по интервалу.

LaTeX

$$$\forall a,b,\; \text{IntervalIntegrable } x \mapsto 1/x$$$

Lean4

theorem intervalIntegrable_one_div (h : ∀ x : ℝ, x ∈ [[a, b]] → f x ≠ 0) (hf : ContinuousOn f [[a, b]]) :
    IntervalIntegrable (fun x => 1 / f x) μ a b :=
  (continuousOn_const.div hf h).intervalIntegrable

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