α : Type u_3
β : Type u_2
M : Type ?u.6116
E : Type ?u.6119
ι : Type u_1
inst✝ : Zero β
s : ι → Set α
f : α → β
a : α
⊢ Tendsto (fun n => indicator (⋃ (i : ι) (_ : i ∈ n), s i) f a) atTop
    (pure (indicator (⋃ (t : Finset ι) (i : ι) (_ : i ∈ t), s i) f a))
α : Type u_3
β : Type u_2
M : Type ?u.6116
E : Type ?u.6119
ι : Type u_1
inst✝ : Zero β
s : ι → Set α
f : α → β
a : α
⊢ Tendsto (fun n => indicator (⋃ (i : ι) (_ : i ∈ n), s i) f a) atTop (pure (indicator (iUnion s) f a))
rw [iUnion_eq_iUnion_finset s]
α : Type u_3
β : Type u_2
M : Type ?u.6116
E : Type ?u.6119
ι : Type u_1
inst✝ : Zero β
s : ι → Set α
f : α → β
a : α
⊢ Monotone fun n => ⋃ (i : ι) (_ : i ∈ n), s i
α : Type u_3
β : Type u_2
M : Type ?u.6116
E : Type ?u.6119
ι : Type u_1
inst✝ : Zero β
s : ι → Set α
f : α → β
a : α
⊢ Tendsto (fun n => indicator (⋃ (i : ι) (_ : i ∈ n), s i) f a) atTop
    (pure (indicator (⋃ (t : Finset ι) (i : ι) (_ : i ∈ t), s i) f a))
refine' Monotone.tendsto_indicator (fun n : Finset ι => ⋃ i ∈ n, s i) _ f a
no goals
α : Type u_3
β : Type u_2
M : Type ?u.6116
E : Type ?u.6119
ι : Type u_1
inst✝ : Zero β
s : ι → Set α
f : α → β
a : α
⊢ Monotone fun n => ⋃ (i : ι) (_ : i ∈ n), s i
exact fun t₁ t₂ => biUnion_subset_biUnion_left