ι : Type ?u.58128
ι' : Type ?u.58131
α : Type ?u.58134
β : Type ?u.58137
γ : Type ?u.58140
P : ℕ → Prop
h : ∀ (a : ℕ), ∃ b, b > a ∧ P b
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
ι : Type ?u.58128
ι' : Type ?u.58131
α : Type ?u.58134
β : Type ?u.58137
γ : Type ?u.58140
P : ℕ → Prop
h : ∃ᶠ (n : ℕ) in atTop, P n
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
rw [frequently_atTop'] at h
no goals
ι : Type ?u.58128
ι' : Type ?u.58131
α : Type ?u.58134
β : Type ?u.58137
γ : Type ?u.58140
P : ℕ → Prop
h : ∀ (a : ℕ), ∃ b, b > a ∧ P b
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
exact extraction_of_frequently_atTop' h