Theorems · Theorem · functional analysis

NormedAddGroupHom.opNorm_eq_of_bounds

∀ {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‖) → (∀ N ≥ 0, (∀ (x : V₁), ‖f x‖ ≤ N * ‖x‖) → M ≤ N) → ‖f‖ = M

Defined in

Mathlib.Analysis.Normed.Group.Hom

Cited by

1 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSeminormedAddCommGroup