case pos
α : Type u_3
β : Type u_2
M : Type ?u.3017
E : Type ?u.3020
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : Zero β
s : ι → Set α
hs : Monotone s
f : α → β
a : α
h : ∃ i, a ∈ s i
⊢ Tendsto (fun i => indicator (s i) f a) atTop (pure (indicator (⋃ (i : ι), s i) f a))

case neg
α : Type u_3
β : Type u_2
M : Type ?u.3017
E : Type ?u.3020
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : Zero β
s : ι → Set α
hs : Monotone s
f : α → β
a : α
h : ¬∃ i, a ∈ s i
⊢ Tendsto (fun i => indicator (s i) f a) atTop (pure (indicator (⋃ (i : ι), s i) f a))
α : Type u_3
β : Type u_2
M : Type ?u.3017
E : Type ?u.3020
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : Zero β
s : ι → Set α
hs : Monotone s
f : α → β
a : α
⊢ Tendsto (fun i => indicator (s i) f a) atTop (pure (indicator (⋃ (i : ι), s i) f a))
by_cases h : ∃ i, a ∈ s i
case pos.intro
α : Type u_3
β : Type u_2
M : Type ?u.3017
E : Type ?u.3020
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : Zero β
s : ι → Set α
hs : Monotone s
f : α → β
a : α
i : ι
hi : a ∈ s i
⊢ Tendsto (fun i => indicator (s i) f a) atTop (pure (indicator (⋃ (i : ι), s i) f a))
case pos
α : Type u_3
β : Type u_2
M : Type ?u.3017
E : Type ?u.3020
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : Zero β
s : ι → Set α
hs : Monotone s
f : α → β
a : α
h : ∃ i, a ∈ s i
⊢ Tendsto (fun i => indicator (s i) f a) atTop (pure (indicator (⋃ (i : ι), s i) f a))
rcases h with ⟨i, hi⟩
case pos.intro
α : Type u_3
β : Type u_2
M : Type ?u.3017
E : Type ?u.3020
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : Zero β
s : ι → Set α
hs : Monotone s
f : α → β
a : α
i : ι
hi : a ∈ s i
n : ι
hn : i ≤ n
⊢ indicator (s n) f a = indicator (⋃ (i : ι), s i) f a
case pos.intro
α : Type u_3
β : Type u_2
M : Type ?u.3017
E : Type ?u.3020
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : Zero β
s : ι → Set α
hs : Monotone s
f : α → β
a : α
i : ι
hi : a ∈ s i
⊢ Tendsto (fun i => indicator (s i) f a) atTop (pure (indicator (⋃ (i : ι), s i) f a))
refine' tendsto_pure.2 ((eventually_ge_atTop i).mono fun n hn => _)
no goals
case pos.intro
α : Type u_3
β : Type u_2
M : Type ?u.3017
E : Type ?u.3020
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : Zero β
s : ι → Set α
hs : Monotone s
f : α → β
a : α
i : ι
hi : a ∈ s i
n : ι
hn : i ≤ n
⊢ indicator (s n) f a = indicator (⋃ (i : ι), s i) f a
rw [indicator_of_mem (hs hn hi) _, indicator_of_mem ((subset_iUnion _ _) hi) _]
case neg
α : Type u_3
β : Type u_2
M : Type ?u.3017
E : Type ?u.3020
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : Zero β
s : ι → Set α
hs : Monotone s
f : α → β
a : α
h : ¬∃ i, a ∈ s i
h' : ¬a ∈ ⋃ (i : ι), s i
⊢ Tendsto (fun i => indicator (s i) f a) atTop (pure (indicator (⋃ (i : ι), s i) f a))
case neg
α : Type u_3
β : Type u_2
M : Type ?u.3017
E : Type ?u.3020
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : Zero β
s : ι → Set α
hs : Monotone s
f : α → β
a : α
h : ¬∃ i, a ∈ s i
⊢ Tendsto (fun i => indicator (s i) f a) atTop (pure (indicator (⋃ (i : ι), s i) f a))
have h' : a ∉ ⋃ i, s i := mt mem_iUnion.1 h
case neg
α : Type u_3
β : Type u_2
M : Type ?u.3017
E : Type ?u.3020
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : Zero β
s : ι → Set α
hs : Monotone s
f : α → β
a : α
h : ∀ (x : ι), ¬a ∈ s x
h' : ¬a ∈ ⋃ (i : ι), s i
⊢ Tendsto (fun i => indicator (s i) f a) atTop (pure (indicator (⋃ (i : ι), s i) f a))
case neg
α : Type u_3
β : Type u_2
M : Type ?u.3017
E : Type ?u.3020
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : Zero β
s : ι → Set α
hs : Monotone s
f : α → β
a : α
h : ¬∃ i, a ∈ s i
h' : ¬a ∈ ⋃ (i : ι), s i
⊢ Tendsto (fun i => indicator (s i) f a) atTop (pure (indicator (⋃ (i : ι), s i) f a))
rw [not_exists] at h
no goals
case neg
α : Type u_3
β : Type u_2
M : Type ?u.3017
E : Type ?u.3020
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : Zero β
s : ι → Set α
hs : Monotone s
f : α → β
a : α
h : ∀ (x : ι), ¬a ∈ s x
h' : ¬a ∈ ⋃ (i : ι), s i
⊢ Tendsto (fun i => indicator (s i) f a) atTop (pure (indicator (⋃ (i : ι), s i) f a))
simpa only [indicator_of_not_mem, *] using tendsto_const_pure