Mathlib Map

Theorems · Theorem · approximation theory

Asymptotics.IsEquivalent.trans_isTheta

∀ {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [inst : NormedAddCommGroup β] [inst_1 : Norm β₂] {l : Filter α}
  {f g₁ : α → β} {g₂ : α → β₂}, Asymptotics.IsEquivalent l f g₁ → g₁ =Θ[l] g₂ → f =Θ[l] g₂
Defined in
Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Cited by
1 results in Mathlib
Foundations
Depth 119 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
NormedAddCommGroupNorm
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

isTheta_choose · cited by 0isTheta_chooseNormedAddCommGroup · cited by 15752NormedAddCommGroupFilter · cited by 8121FilterNorm · cited by 512NormAsymptotics.IsTheta · cited by 115Asymptotics.IsThetaAsymptotics.IsEquivalent · cited by 98Asymptotics.IsEquivalentAsymptotics.IsEquivalent.isTheta · cited by 9IsEquivalent.isThetaAsymptotics.IsTheta.trans · cited by 3IsTheta.transIsEquivalent.trans_isThetaCITED BYCITES

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.