intervalIntegrable_inv — Mathlib

English

The reciprocal function on an interval not containing zero is interval-integrable.

Русский

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

LaTeX

$$$\text{IntervalIntegrable } (f(x))^{-1} $ на интервале без нуля$$

Lean4

@[simp]
theorem intervalIntegrable_inv (h : ∀ x : ℝ, x ∈ [[a, b]] → f x ≠ 0) (hf : ContinuousOn f [[a, b]]) :
    IntervalIntegrable (fun x => (f x)⁻¹) μ a b := by simpa only [one_div] using intervalIntegrable_one_div h hf

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