α : Type u_2
β : Type ?u.360947
γ : Type ?u.360950
δ : Type ?u.360953
ι : Type u_1
R : Type ?u.360959
R' : Type ?u.360962
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
inst✝ : Countable ι
s : ι → Set α
t : Set α
ht : MeasurableSet t
⊢ ↑↑(restrict μ (⋃ (i : ι), s i)) t ≤ ↑↑(sum fun i => restrict μ (s i)) t
α : Type u_2
β : Type ?u.360947
γ : Type ?u.360950
δ : Type ?u.360953
ι : Type u_1
R : Type ?u.360959
R' : Type ?u.360962
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : Countable ι
s : ι → Set α
⊢ restrict μ (⋃ (i : ι), s i) ≤ sum fun i => restrict μ (s i)
intro t ht
α : Type u_2
β : Type ?u.360947
γ : Type ?u.360950
δ : Type ?u.360953
ι : Type u_1
R : Type ?u.360959
R' : Type ?u.360962
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
inst✝ : Countable ι
s : ι → Set α
t : Set α
ht : MeasurableSet t
⊢ ↑↑μ (⋃ (i : ι), t ∩ s i) ≤ ∑' (i : ι), ↑↑μ (t ∩ s i)
α : Type u_2
β : Type ?u.360947
γ : Type ?u.360950
δ : Type ?u.360953
ι : Type u_1
R : Type ?u.360959
R' : Type ?u.360962
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
inst✝ : Countable ι
s : ι → Set α
t : Set α
ht : MeasurableSet t
⊢ ↑↑(restrict μ (⋃ (i : ι), s i)) t ≤ ↑↑(sum fun i => restrict μ (s i)) t
suffices μ (⋃ i, t ∩ s i) ≤ ∑' i, μ (t ∩ s i) by simpa [ht, inter_iUnion]
no goals
α : Type u_2
β : Type ?u.360947
γ : Type ?u.360950
δ : Type ?u.360953
ι : Type u_1
R : Type ?u.360959
R' : Type ?u.360962
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
inst✝ : Countable ι
s : ι → Set α
t : Set α
ht : MeasurableSet t
⊢ ↑↑μ (⋃ (i : ι), t ∩ s i) ≤ ∑' (i : ι), ↑↑μ (t ∩ s i)
apply measure_iUnion_le
no goals
α : Type u_2
β : Type ?u.360947
γ : Type ?u.360950
δ : Type ?u.360953
ι : Type u_1
R : Type ?u.360959
R' : Type ?u.360962
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
inst✝ : Countable ι
s : ι → Set α
t : Set α
ht : MeasurableSet t
this : ↑↑μ (⋃ (i : ι), t ∩ s i) ≤ ∑' (i : ι), ↑↑μ (t ∩ s i)
⊢ ↑↑(restrict μ (⋃ (i : ι), s i)) t ≤ ↑↑(sum fun i => restrict μ (s i)) t
simpa [ht, inter_iUnion]