∀ (g : ℝ → ℝ) (basis_begin : List (ℝ → ℝ)) (basis_end : ℝ → ℝ),
  g ∈ basis_begin →
    (List.Pairwise (fun x y => (Real.log ∘ y) =o[Filter.atTop] (Real.log ∘ x)) (basis_begin ++ [basis_end]) ∧
        ∀ (f : ℝ → ℝ), f ∈ basis_begin ∨ f = basis_end → Filter.Tendsto f Filter.atTop Filter.atTop) →
      (Real.log ∘ basis_end) =o[Filter.atTop] (Real.log ∘ g)