α : Type u_2
β : Type ?u.58576
γ : Type ?u.58579
δ : Type ?u.58582
ι : Type u_1
R : Type ?u.58588
R' : Type ?u.58591
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝¹ : Countable ι
inst✝ : SemilatticeSup ι
s : ι → Set α
hs : ∀ (n : ι), MeasurableSet (s n)
hm : Antitone s
hf : ∃ i, ↑↑μ (s i) ≠ ⊤
⊢ Tendsto (↑↑μ ∘ s) atTop (𝓝 (⨅ (i : ι), ↑↑μ (s i)))
α : Type u_2
β : Type ?u.58576
γ : Type ?u.58579
δ : Type ?u.58582
ι : Type u_1
R : Type ?u.58588
R' : Type ?u.58591
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝¹ : Countable ι
inst✝ : SemilatticeSup ι
s : ι → Set α
hs : ∀ (n : ι), MeasurableSet (s n)
hm : Antitone s
hf : ∃ i, ↑↑μ (s i) ≠ ⊤
⊢ Tendsto (↑↑μ ∘ s) atTop (𝓝 (↑↑μ (⋂ (n : ι), s n)))
rw [measure_iInter_eq_iInf hs (directed_of_sup hm) hf]
no goals
α : Type u_2
β : Type ?u.58576
γ : Type ?u.58579
δ : Type ?u.58582
ι : Type u_1
R : Type ?u.58588
R' : Type ?u.58591
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝¹ : Countable ι
inst✝ : SemilatticeSup ι
s : ι → Set α
hs : ∀ (n : ι), MeasurableSet (s n)
hm : Antitone s
hf : ∃ i, ↑↑μ (s i) ≠ ⊤
⊢ Tendsto (↑↑μ ∘ s) atTop (𝓝 (⨅ (i : ι), ↑↑μ (s i)))
exact tendsto_atTop_iInf fun n m hnm => measure_mono <| hm hnm