Theorems · Theorem · approximation theory

Asymptotics.IsLittleO.add_add

∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {l : Filter α} {f₁ f₂ : α → E'} {g₁ g₂ : α → F'},
  f₁ =o[l] g₁ → f₂ =o[l] g₂ → (fun x => f₁ x + f₂ x) =o[l] fun x => ‖g₁ x‖ + ‖g₂ x‖

Defined in

Mathlib.Analysis.Asymptotics.Defs

Cited by

3 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSeminormedAddCommGroup