case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2273791
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
⊢ ∀ (a : α),
    (∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v a) (𝓝 c)) →
      Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v a) (𝓝 (limRatio v ρ a))
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2273791
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatio v ρ x))
filter_upwards [v.ae_tendsto_div hρ]
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2273791
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
hx : ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)
⊢ Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatio v ρ x))
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2273791
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
⊢ ∀ (a : α),
    (∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v a) (𝓝 c)) →
      Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v a) (𝓝 (limRatio v ρ a))
intro x hx
no goals
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2273791
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
hx : ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)
⊢ Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatio v ρ x))
exact tendsto_nhds_limUnder hx