α : Type u_1
β : Type ?u.299320
γ : Type ?u.299323
δ : Type ?u.299326
ι : Type ?u.299329
R : Type ?u.299332
R' : Type ?u.299335
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s'✝ t✝ s s' t : Set α
ht : MeasurableSet t
⊢ ↑↑(restrict μ (s ∪ s')) t ≤ ↑↑(restrict μ s + restrict μ s') t
α : Type u_1
β : Type ?u.299320
γ : Type ?u.299323
δ : Type ?u.299326
ι : Type ?u.299329
R : Type ?u.299332
R' : Type ?u.299335
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s'✝ t s s' : Set α
⊢ restrict μ (s ∪ s') ≤ restrict μ s + restrict μ s'
intro t ht
α : Type u_1
β : Type ?u.299320
γ : Type ?u.299323
δ : Type ?u.299326
ι : Type ?u.299329
R : Type ?u.299332
R' : Type ?u.299335
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s'✝ t✝ s s' t : Set α
ht : MeasurableSet t
⊢ ↑↑μ (t ∩ s ∪ t ∩ s') ≤ ↑↑μ (t ∩ s) + ↑↑μ (t ∩ s')
α : Type u_1
β : Type ?u.299320
γ : Type ?u.299323
δ : Type ?u.299326
ι : Type ?u.299329
R : Type ?u.299332
R' : Type ?u.299335
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s'✝ t✝ s s' t : Set α
ht : MeasurableSet t
⊢ ↑↑(restrict μ (s ∪ s')) t ≤ ↑↑(restrict μ s + restrict μ s') t
suffices μ (t ∩ s ∪ t ∩ s') ≤ μ (t ∩ s) + μ (t ∩ s') by simpa [ht, inter_union_distrib_left]
no goals
α : Type u_1
β : Type ?u.299320
γ : Type ?u.299323
δ : Type ?u.299326
ι : Type ?u.299329
R : Type ?u.299332
R' : Type ?u.299335
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s'✝ t✝ s s' t : Set α
ht : MeasurableSet t
⊢ ↑↑μ (t ∩ s ∪ t ∩ s') ≤ ↑↑μ (t ∩ s) + ↑↑μ (t ∩ s')
apply measure_union_le
no goals
α : Type u_1
β : Type ?u.299320
γ : Type ?u.299323
δ : Type ?u.299326
ι : Type ?u.299329
R : Type ?u.299332
R' : Type ?u.299335
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s'✝ t✝ s s' t : Set α
ht : MeasurableSet t
this : ↑↑μ (t ∩ s ∪ t ∩ s') ≤ ↑↑μ (t ∩ s) + ↑↑μ (t ∩ s')
⊢ ↑↑(restrict μ (s ∪ s')) t ≤ ↑↑(restrict μ s + restrict μ s') t
simpa [ht, inter_union_distrib_left]