α : Type u_2
β : Type ?u.56609
γ : Type ?u.56612
δ : Type ?u.56615
ι : Type u_1
R : Type ?u.56621
R' : Type ?u.56624
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
s : ι → Set α
hm : Monotone s
⊢ Tendsto (↑↑μ ∘ s) atTop (𝓝 (⨆ (i : ι), ↑↑μ (s i)))
α : Type u_2
β : Type ?u.56609
γ : Type ?u.56612
δ : Type ?u.56615
ι : Type u_1
R : Type ?u.56621
R' : Type ?u.56624
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
s : ι → Set α
hm : Monotone s
⊢ Tendsto (↑↑μ ∘ s) atTop (𝓝 (↑↑μ (⋃ (n : ι), s n)))
rw [measure_iUnion_eq_iSup (directed_of_sup hm)]
no goals
α : Type u_2
β : Type ?u.56609
γ : Type ?u.56612
δ : Type ?u.56615
ι : Type u_1
R : Type ?u.56621
R' : Type ?u.56624
m : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t : Set α
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
s : ι → Set α
hm : Monotone s
⊢ Tendsto (↑↑μ ∘ s) atTop (𝓝 (⨆ (i : ι), ↑↑μ (s i)))
exact tendsto_atTop_iSup fun n m hnm => measure_mono <| hm hnm