Theorem: MeasureTheory.nonempty_inter_of_measureReal_lt_add (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 α
m : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real s + μ.real t
hu : autoParam (μ u ≠ ⊤) _auto✝
⊢ (s ∩ t).Nonempty
Tactic:
apply nonempty_inter_of_measure_lt_add μ ht h's h't
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : 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 : μ.real u < μ.real s + μ.real t
hu : autoParam (μ u ≠ ⊤) _auto✝
⊢ μ u < μ s + μ t

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : 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 : μ.real u < μ.real s + μ.real t
hu : autoParam (μ u ≠ ⊤) _auto✝
⊢ μ u < μ s + μ t
Tactic:
apply (ENNReal.toReal_lt_toReal hu _).1
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : 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 : μ.real u < μ.real s + μ.real t
hu : autoParam (μ u ≠ ⊤) _auto✝
⊢ (μ u).toReal < (μ s + μ t).toReal

ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : 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 : μ.real u < μ.real s + μ.real t
hu : autoParam (μ u ≠ ⊤) _auto✝
⊢ μ s + μ t ≠ ⊤

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : 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 : μ.real u < μ.real s + μ.real t
hu : autoParam (μ u ≠ ⊤) _auto✝
⊢ (μ u).toReal < (μ s + μ t).toReal
Tactic:
rw [ENNReal.toReal_add (measure_ne_top_of_subset h's hu) (measure_ne_top_of_subset h't hu)]
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : 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 : μ.real u < μ.real s + μ.real t
hu : autoParam (μ u ≠ ⊤) _auto✝
⊢ (μ u).toReal < (μ s).toReal + (μ t).toReal

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : 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 : μ.real u < μ.real s + μ.real t
hu : autoParam (μ u ≠ ⊤) _auto✝
⊢ (μ u).toReal < (μ s).toReal + (μ t).toReal
Tactic:
exact h
State after:
no goals

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : 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 : μ.real u < μ.real s + μ.real t
hu : autoParam (μ u ≠ ⊤) _auto✝
⊢ μ s + μ t ≠ ⊤
Tactic:
exact ENNReal.add_ne_top.2 ⟨measure_ne_top_of_subset h's hu, measure_ne_top_of_subset h't hu⟩
State after:
no goals