∀ {α : Type u_1} {E : Type u_3} (F : Type u_4) [inst : Norm E] [inst_1 : Norm F] {f : α → E} {l : Filter α}
  [inst_2 : One F] [NormOneClass F],
  (f =O[l] fun _x => 1) = Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖f x‖