α : Type u_1
β : Type ?u.69212
γ : Type ?u.69215
δ : Type ?u.69218
m✝ : MeasurableSpace α
μ✝ ν : Measure α
m : MeasurableSpace α
f : α →ₛ ℝ≥0∞
μ : Measure α
⊢ (⨆ (g : α →ₛ ℝ≥0∞) (_ : ↑g ≤ fun a => ↑f a), lintegral g μ) = lintegral f μ
α : Type u_1
β : Type ?u.69212
γ : Type ?u.69215
δ : Type ?u.69218
m✝ : MeasurableSpace α
μ✝ ν : Measure α
m : MeasurableSpace α
f : α →ₛ ℝ≥0∞
μ : Measure α
⊢ (∫⁻ (a : α), ↑f a ∂μ) = lintegral f μ
rw [MeasureTheory.lintegral]
no goals
α : Type u_1
β : Type ?u.69212
γ : Type ?u.69215
δ : Type ?u.69218
m✝ : MeasurableSpace α
μ✝ ν : Measure α
m : MeasurableSpace α
f : α →ₛ ℝ≥0∞
μ : Measure α
⊢ (⨆ (g : α →ₛ ℝ≥0∞) (_ : ↑g ≤ fun a => ↑f a), lintegral g μ) = lintegral f μ
exact
  le_antisymm (iSup₂_le fun g hg => lintegral_mono hg <| le_rfl) (le_iSup₂_of_le f le_rfl le_rfl)