Theorems · Theorem · real analysis

Asymptotics.IsTheta.isBoundedUnder_le_iff

∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {f' : α → E'} {g' : α → F'} {l : Filter α},
  f' =Θ[l] g' →
    (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ f') ↔
      Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ g'))

Defined in

Mathlib.Analysis.Asymptotics.Theta

Cited by

0 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSeminormedAddCommGroup