ι : Type ?u.269296
ι' : Type ?u.269299
α : Type u_2
β : Type u_1
γ : Type ?u.269308
inst✝ : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ n, x ∈ f n
⊢ ∀ (i : α), ∀ᶠ (a : β) in atTop, f a ∈ Ici {i}
ι : Type ?u.269296
ι' : Type ?u.269299
α : Type u_2
β : Type u_1
γ : Type ?u.269308
inst✝ : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ n, x ∈ f n
⊢ Tendsto f atTop atTop
simp only [atTop_finset_eq_iInf, tendsto_iInf, tendsto_principal]
ι : Type ?u.269296
ι' : Type ?u.269299
α : Type u_2
β : Type u_1
γ : Type ?u.269308
inst✝ : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ n, x ∈ f n
a : α
⊢ ∀ᶠ (a_1 : β) in atTop, f a_1 ∈ Ici {a}
ι : Type ?u.269296
ι' : Type ?u.269299
α : Type u_2
β : Type u_1
γ : Type ?u.269308
inst✝ : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ n, x ∈ f n
⊢ ∀ (i : α), ∀ᶠ (a : β) in atTop, f a ∈ Ici {i}
intro a
case intro
ι : Type ?u.269296
ι' : Type ?u.269299
α : Type u_2
β : Type u_1
γ : Type ?u.269308
inst✝ : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ n, x ∈ f n
a : α
b : β
hb : a ∈ f b
⊢ ∀ᶠ (a_1 : β) in atTop, f a_1 ∈ Ici {a}
ι : Type ?u.269296
ι' : Type ?u.269299
α : Type u_2
β : Type u_1
γ : Type ?u.269308
inst✝ : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ n, x ∈ f n
a : α
⊢ ∀ᶠ (a_1 : β) in atTop, f a_1 ∈ Ici {a}
rcases h' a with ⟨b, hb⟩
no goals
case intro
ι : Type ?u.269296
ι' : Type ?u.269299
α : Type u_2
β : Type u_1
γ : Type ?u.269308
inst✝ : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ n, x ∈ f n
a : α
b : β
hb : a ∈ f b
⊢ ∀ᶠ (a_1 : β) in atTop, f a_1 ∈ Ici {a}
exact (eventually_ge_atTop b).mono fun b' hb' => (Finset.singleton_subset_iff.2 hb).trans (h hb')