Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
R : Type ?u.49329
inst✝⁴ : SMul R ℝ≥0
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : TopologicalSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
f_le_g : ↑f ≤ ↑g
⊢ (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ) ≤ ∫⁻ (ω : Ω), ↑(↑g ω) ∂↑μ
Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
R : Type ?u.49329
inst✝⁴ : SMul R ℝ≥0
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : TopologicalSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
f_le_g : ↑f ≤ ↑g
⊢ testAgainstNN μ f ≤ testAgainstNN μ g
simp only [← ENNReal.coe_le_coe, testAgainstNN_coe_eq]
no goals
Ω : Type u_1
inst✝⁵ : MeasurableSpace Ω
R : Type ?u.49329
inst✝⁴ : SMul R ℝ≥0
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : TopologicalSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
f_le_g : ↑f ≤ ↑g
⊢ (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ) ≤ ∫⁻ (ω : Ω), ↑(↑g ω) ∂↑μ
exact lintegral_mono fun ω => ENNReal.coe_mono (f_le_g ω)