Theorems · Theorem · approximation theory

Asymptotics.IsTheta.trans_isEquivalent

∀ {α : Type u_1} {β : Type u_2} {β₂ : Type u_3} [inst : NormedAddCommGroup β] [inst_1 : Norm β₂] {l : Filter α}
  {f : α → β₂} {g₁ g₂ : α → β}, f =Θ[l] g₁ → Asymptotics.IsEquivalent l g₁ g₂ → f =Θ[l] g₂

Defined in

Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNorm