Theorems · Theorem · real analysis

Asymptotics.IsTheta.isTheta_congr_right

∀ {α : Type u_1} {G : Type u_5} {E' : Type u_6} {F' : Type u_7} [inst : Norm G] [inst_1 : SeminormedAddCommGroup E']
  [inst_2 : SeminormedAddCommGroup F'] {k : α → G} {f' : α → E'} {g' : α → F'} {l : Filter α},
  f' =Θ[l] g' → (k =Θ[l] f' ↔ k =Θ[l] g')

Defined in

Mathlib.Analysis.Asymptotics.Theta

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormSeminormedAddCommGroupSeminormedAddCommGroup