ι✝ : Type ?u.371220
ι' : Type ?u.371223
α : Type ?u.371226
β : Type ?u.371229
γ : Type ?u.371232
ι : Type u_1
x : ℕ → ι
p : ι → Prop
l : Filter ι
h_tendsto : ∀ (x_1 : ℕ → ℕ), Tendsto x_1 atTop atTop → Tendsto (x ∘ x_1) atTop l
h : ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ ns, Tendsto (fun n => x (ns n)) atTop l ∧ ∀ (n : ℕ), p (x (ns n))
ι✝ : Type ?u.371220
ι' : Type ?u.371223
α : Type ?u.371226
β : Type ?u.371229
γ : Type ?u.371232
ι : Type u_1
x : ℕ → ι
p : ι → Prop
l : Filter ι
h_tendsto : Tendsto x atTop l
h : ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ ns, Tendsto (fun n => x (ns n)) atTop l ∧ ∀ (n : ℕ), p (x (ns n))
rw [tendsto_iff_seq_tendsto] at h_tendsto
ι✝ : Type ?u.371220
ι' : Type ?u.371223
α : Type ?u.371226
β : Type ?u.371229
γ : Type ?u.371232
ι : Type u_1
x : ℕ → ι
p : ι → Prop
l : Filter ι
h_tendsto : ∀ (x_1 : ℕ → ℕ), Tendsto x_1 atTop atTop → Tendsto (x ∘ x_1) atTop l
h : ∃ᶠ (n : ℕ) in atTop, p (x n)
ns : ℕ → ℕ
hge : ∀ (a : ℕ), ns a ≥ a
hns : ∀ (a : ℕ), p (x (ns a))
⊢ ∃ ns, Tendsto (fun n => x (ns n)) atTop l ∧ ∀ (n : ℕ), p (x (ns n))
ι✝ : Type ?u.371220
ι' : Type ?u.371223
α : Type ?u.371226
β : Type ?u.371229
γ : Type ?u.371232
ι : Type u_1
x : ℕ → ι
p : ι → Prop
l : Filter ι
h_tendsto : ∀ (x_1 : ℕ → ℕ), Tendsto x_1 atTop atTop → Tendsto (x ∘ x_1) atTop l
h : ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ ns, Tendsto (fun n => x (ns n)) atTop l ∧ ∀ (n : ℕ), p (x (ns n))
choose ns hge hns using frequently_atTop.1 h
no goals
ι✝ : Type ?u.371220
ι' : Type ?u.371223
α : Type ?u.371226
β : Type ?u.371229
γ : Type ?u.371232
ι : Type u_1
x : ℕ → ι
p : ι → Prop
l : Filter ι
h_tendsto : ∀ (x_1 : ℕ → ℕ), Tendsto x_1 atTop atTop → Tendsto (x ∘ x_1) atTop l
h : ∃ᶠ (n : ℕ) in atTop, p (x n)
ns : ℕ → ℕ
hge : ∀ (a : ℕ), ns a ≥ a
hns : ∀ (a : ℕ), p (x (ns a))
⊢ ∃ ns, Tendsto (fun n => x (ns n)) atTop l ∧ ∀ (n : ℕ), p (x (ns n))
exact ⟨ns, h_tendsto ns (tendsto_atTop_mono hge tendsto_id), hns⟩