lintegral_le_meas — Mathlib

English

If f ≤ 1 everywhere and f = 0 outside s, then ∫ f dμ ≤ μ(s).

Русский

Если f ≤ 1 везде и f=0 вне s, то ∫ f dμ ≤ μ(s).

LaTeX

$$$$ \int f \! dμ ≤ μ(s), \quad f ≤ 1, \ f|_{s^c}=0. $$$$

Lean4

theorem lintegral_le_meas {s : Set α} {f : α → ℝ≥0∞} (hf : ∀ a, f a ≤ 1) (h'f : ∀ a ∈ sᶜ, f a = 0) :
    ∫⁻ a, f a ∂μ ≤ μ s :=
  by
  apply (lintegral_mono (fun x ↦ ?_)).trans (lintegral_indicator_one_le s)
  by_cases hx : x ∈ s
  · simpa [hx] using hf x
  · simpa [hx] using h'f x hx

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