Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
s₁ s₂ : Set Ω
h : s₁ ⊆ s₂
⊢ ENNReal.toNNReal (↑↑↑μ s₁) ≤ ENNReal.toNNReal (↑↑↑μ s₂)
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
s₁ s₂ : Set Ω
h : s₁ ⊆ s₂
⊢ (fun s => ENNReal.toNNReal (↑↑↑μ s)) s₁ ≤ (fun s => ENNReal.toNNReal (↑↑↑μ s)) s₂
change ((μ : Measure Ω) s₁).toNNReal ≤ ((μ : Measure Ω) s₂).toNNReal
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
s₁ s₂ : Set Ω
h : s₁ ⊆ s₂
key : ↑↑↑μ s₁ ≤ ↑↑↑μ s₂
⊢ ENNReal.toNNReal (↑↑↑μ s₁) ≤ ENNReal.toNNReal (↑↑↑μ s₂)
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
s₁ s₂ : Set Ω
h : s₁ ⊆ s₂
⊢ ENNReal.toNNReal (↑↑↑μ s₁) ≤ ENNReal.toNNReal (↑↑↑μ s₂)
have key : (μ : Measure Ω) s₁ ≤ (μ : Measure Ω) s₂ := (μ : Measure Ω).mono h
no goals
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ : FiniteMeasure Ω
s₁ s₂ : Set Ω
h : s₁ ⊆ s₂
key : ↑↑↑μ s₁ ≤ ↑↑↑μ s₂
⊢ ENNReal.toNNReal (↑↑↑μ s₁) ≤ ENNReal.toNNReal (↑↑↑μ s₂)
apply (ENNReal.toNNReal_le_toNNReal (measure_ne_top _ s₁) (measure_ne_top _ s₂)).mpr key