Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s₁ s₂ : Set Ω
h : s₁ ⊆ s₂
⊢ (fun s => ENNReal.toNNReal (↑↑↑(toFiniteMeasure μ) s)) s₁ ≤ (fun s => ENNReal.toNNReal (↑↑↑(toFiniteMeasure μ) s)) s₂
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s₁ s₂ : Set Ω
h : s₁ ⊆ s₂
⊢ (fun s => ENNReal.toNNReal (↑↑↑μ s)) s₁ ≤ (fun s => ENNReal.toNNReal (↑↑↑μ s)) s₂
rw [← coeFn_comp_toFiniteMeasure_eq_coeFn]
no goals
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s₁ s₂ : Set Ω
h : s₁ ⊆ s₂
⊢ (fun s => ENNReal.toNNReal (↑↑↑(toFiniteMeasure μ) s)) s₁ ≤ (fun s => ENNReal.toNNReal (↑↑↑(toFiniteMeasure μ) s)) s₂
exact MeasureTheory.FiniteMeasure.apply_mono _ h