intro ε hε
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
h : Tendsto g atTop (nhds 0)
⊢ ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : α), N ≤ n → |f n| < ε
α : Type u_1
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f g : α → ℝ
hfg : ∀ (x : α), |f x| ≤ g x
h : Tendsto g atTop (nhds 0)
ε : ℝ
hε : 0 < ε
⊢ ∃ N, ∀ (n : α), N ≤ n → |f n| < ε