α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2775341
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
⊢ ∃ u v_1,
    MeasurableSet u ∧
      MeasurableSet v_1 ∧ {x | limRatio v ρ x < ↑p} ⊆ u ∧ {x | ↑q < limRatio v ρ x} ⊆ v_1 ∧ ↑↑μ (u ∩ v_1) = 0
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2775341
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
⊢ AEMeasurable (limRatio v ρ)
apply ENNReal.aemeasurable_of_exist_almost_disjoint_supersets _ _ fun p q hpq => ?_
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2775341
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
⊢ ∃ u v_1,
    MeasurableSet u ∧
      MeasurableSet v_1 ∧ {x | limRatio v ρ x < ↑p} ⊆ u ∧ {x | ↑q < limRatio v ρ x} ⊆ v_1 ∧ ↑↑μ (u ∩ v_1) = 0
exact v.exists_measurable_supersets_limRatio hρ hpq