Theorems · Theorem · functional analysis

NormedAddGroupHom.opNorm_le_bound

∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f : NormedAddGroupHom V₁ V₂) {M : ℝ}, 0 ≤ M → (∀ (x : V₁), ‖f x‖ ≤ M * ‖x‖) → ‖f‖ ≤ M

If one controls the norm of every f x, then one controls the norm of f.

Defined in

Mathlib.Analysis.Normed.Group.Hom

Cited by

12 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSeminormedAddCommGroup