α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
h : u =O[l] 0
⊢ u ~[l] 0
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
⊢ u ~[l] 0 ↔ u =O[l] 0
refine' ⟨IsEquivalent.isBigO, fun h ↦ _⟩
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
h : u =O[l] 0
⊢ ∃ s, s ∈ l ∧ Set.EqOn u 0 s
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
h : u =O[l] 0
⊢ u ~[l] 0
rw [isEquivalent_zero_iff_eventually_zero, eventuallyEq_iff_exists_mem]
no goals
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v w : α → β
l : Filter α
h : u =O[l] 0
⊢ ∃ s, s ∈ l ∧ Set.EqOn u 0 s
exact ⟨{ x : α | u x = 0 }, isBigO_zero_right_iff.mp h, fun x hx ↦ hx⟩