α : Type u_1
β : Type ?u.43834
γ : Type ?u.43837
δ : Type ?u.43840
ι : Type ?u.43843
R : Type ?u.43846
R' : Type ?u.43849
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : ↑↑μ u < ↑↑μ s + ↑↑μ t
⊢ ¬Disjoint s t
α : Type u_1
β : Type ?u.43834
γ : Type ?u.43837
δ : Type ?u.43840
ι : Type ?u.43843
R : Type ?u.43846
R' : Type ?u.43849
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : ↑↑μ u < ↑↑μ s + ↑↑μ t
⊢ Set.Nonempty (s ∩ t)
rw [← Set.not_disjoint_iff_nonempty_inter]
α : Type u_1
β : Type ?u.43834
γ : Type ?u.43837
δ : Type ?u.43840
ι : Type ?u.43843
R : Type ?u.43846
R' : Type ?u.43849
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : Disjoint s t
⊢ ↑↑μ s + ↑↑μ t ≤ ↑↑μ u
α : Type u_1
β : Type ?u.43834
γ : Type ?u.43837
δ : Type ?u.43840
ι : Type ?u.43843
R : Type ?u.43846
R' : Type ?u.43849
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : ↑↑μ u < ↑↑μ s + ↑↑μ t
⊢ ¬Disjoint s t
contrapose! h
no goals
α : Type u_1
β : Type ?u.43834
γ : Type ?u.43837
δ : Type ?u.43840
ι : Type ?u.43843
R : Type ?u.43846
R' : Type ?u.43849
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : Disjoint s t
⊢ ↑↑μ s + ↑↑μ t ≤ ↑↑μ u
calc
  μ s + μ t = μ (s ∪ t) := (measure_union h ht).symm
  _ ≤ μ u := measure_mono (union_subset h's h't)