Theorems · Theorem · functional analysis

Filter.Tendsto.op_zero_isBoundedUnder_le

∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : SeminormedAddGroup E]
  [inst_1 : SeminormedAddGroup F] [inst_2 : SeminormedAddGroup G] {f : α → E} {g : α → F} {l : Filter α},
  Filter.Tendsto f l (nhds 0) →
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l (norm ∘ g) →
      ∀ (op : E → F → G),
        (∀ (x : E) (y : F), ‖op x y‖ ≤ ‖x‖ * ‖y‖) → Filter.Tendsto (fun x => op (f x) (g x)) l (nhds 0)

A helper lemma used to prove that the (scalar or usual) product of a function that tends to zero and a bounded function tends to zero. This lemma is formulated for any binary operation op : E → F → G with an estimate ‖op x y‖ ≤ ‖x‖ * ‖y‖ instead of multiplication so that it can be applied to (*), flip (*), (•), and flip (•).

Defined in

Mathlib.Analysis.Normed.Group.Bounded

Cited by

4 results in Mathlib

Foundations

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

Assumes

SeminormedAddGroupSeminormedAddGroupSeminormedAddGroup