div_const — Mathlib

English

If f is interval integrable on [a,b] with respect to μ, then the function x ↦ f(x) / c is interval integrable on [a,b] for any constant c.

Русский

Если f(interval) интегрируема на [a,b] по отношению к μ, то функция x ↦ f(x)/c интегрируема на [a,b] для любого константного c.

LaTeX

$$$IntervalIntegrable(f, μ, a, b) \\Rightarrow IntervalIntegrable(x \\mapsto f(x)/c, μ, a, b)$$$

Lean4

@[simp]
theorem div_const {𝕜 : Type*} {f : ℝ → 𝕜} [NormedDivisionRing 𝕜] (h : IntervalIntegrable f μ a b) (c : 𝕜) :
    IntervalIntegrable (fun x => f x / c) μ a b := by simpa only [div_eq_mul_inv] using mul_const h c⁻¹

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