Theorems · Theorem · approximation theory

Asymptotics.IsEquivalent.eventually_neg

∀ {α : Type u_1} {β : Type u_2} [inst : NormedField β] [inst_1 : LinearOrder β] [IsStrictOrderedRing β] {u v : α → β}
  {l : Filter α} [ClosedIicTopology β],
  Asymptotics.IsEquivalent l u v → (∀ᶠ (t : α) in l, v t < 0) → ∀ᶠ (x : α) in l, u x < 0

Defined in

Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Cited by

0 results in Mathlib

Foundations

Depth 169 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedFieldLinearOrderIsStrictOrderedRingClosedIicTopology