Theorem: MeasureTheory.sum_measureReal_le_measureReal_univ (Carleson/ToMathlib/MeasureReal.lean)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ : Set α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (↑s).PairwiseDisjoint t
⊢ ∑ i ∈ s, μ.real (t i) ≤ μ.real univ
Tactic:
simp only [measureReal_def]
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ : Set α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (↑s).PairwiseDisjoint t
⊢ ∑ x ∈ s, (μ (t x)).toReal ≤ (μ univ).toReal

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ : Set α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (↑s).PairwiseDisjoint t
⊢ ∑ x ∈ s, (μ (t x)).toReal ≤ (μ univ).toReal
Tactic:
rw [← ENNReal.toReal_sum (fun i hi ↦ measure_ne_top _ _)]
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ : Set α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (↑s).PairwiseDisjoint t
⊢ (∑ a ∈ s, μ (t a)).toReal ≤ (μ univ).toReal

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ : Set α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (↑s).PairwiseDisjoint t
⊢ (∑ a ∈ s, μ (t a)).toReal ≤ (μ univ).toReal
Tactic:
apply ENNReal.toReal_mono (measure_ne_top _ _)
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ : Set α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (↑s).PairwiseDisjoint t
⊢ ∑ a ∈ s, μ (t a) ≤ μ univ

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t✝ : Set α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (↑s).PairwiseDisjoint t
⊢ ∑ a ∈ s, μ (t a) ≤ μ univ
Tactic:
exact sum_measure_le_measure_univ h H
State after:
no goals