lintegral_coe_le_coe_iff_integral_le

English

For nonnegative f: α → ℝ≥0 with Integrable (f ∘) and any b ∈ ℝ≥0, the Lintegral comparison with a real bound is equivalent to the real integral bound: ∫⁻ f ≤ b iff ∫ f ≤ b.

Русский

Для неотрицательной f: α → ℝ≥0 с Integrable и любого b ∈ ℝ≥0, сравнение Lintegral с верхней гранью в действительных числах эквивалентно ограничению интеграла: ∫⁻ f ≤ b ⇔ ∫ f ≤ b.

LaTeX

$$$\\\\int⁻ a \\, f(a) \\, d\\\\mu \\\\le b \\\\iff \\\\int a \\, (f(a)) \\\\le b$$$

Lean4

theorem lintegral_coe_le_coe_iff_integral_le {f : α → ℝ≥0} (hfi : Integrable (fun x => (f x : ℝ)) μ) {b : ℝ≥0} :
    ∫⁻ a, f a ∂μ ≤ b ↔ ∫ a, (f a : ℝ) ∂μ ≤ b := by
  rw [lintegral_coe_eq_integral f hfi, ENNReal.ofReal, ENNReal.coe_le_coe, Real.toNNReal_le_iff_le_coe]

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