α : Type u_1
β : Type ?u.45468
γ : Type ?u.45471
δ : Type ?u.45474
ι : Type ?u.45477
R : Type ?u.45480
R' : Type ?u.45483
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : ↑↑μ u < ↑↑μ t + ↑↑μ s
⊢ Set.Nonempty (s ∩ t)
α : Type u_1
β : Type ?u.45468
γ : Type ?u.45471
δ : Type ?u.45474
ι : Type ?u.45477
R : Type ?u.45480
R' : Type ?u.45483
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : ↑↑μ u < ↑↑μ s + ↑↑μ t
⊢ Set.Nonempty (s ∩ t)
rw [add_comm] at h
α : Type u_1
β : Type ?u.45468
γ : Type ?u.45471
δ : Type ?u.45474
ι : Type ?u.45477
R : Type ?u.45480
R' : Type ?u.45483
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : ↑↑μ u < ↑↑μ t + ↑↑μ s
⊢ Set.Nonempty (t ∩ s)
α : Type u_1
β : Type ?u.45468
γ : Type ?u.45471
δ : Type ?u.45474
ι : Type ?u.45477
R : Type ?u.45480
R' : Type ?u.45483
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : ↑↑μ u < ↑↑μ t + ↑↑μ s
⊢ Set.Nonempty (s ∩ t)
rw [inter_comm]
no goals
α : Type u_1
β : Type ?u.45468
γ : Type ?u.45471
δ : Type ?u.45474
ι : Type ?u.45477
R : Type ?u.45480
R' : Type ?u.45483
m✝ : MeasurableSpace α
μ✝ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t✝ : Set α
m : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : ↑↑μ u < ↑↑μ t + ↑↑μ s
⊢ Set.Nonempty (t ∩ s)
exact nonempty_inter_of_measure_lt_add μ hs h't h's h