Theorems · Theorem · functional analysis

LinearMap.mkContinuous_norm_le

∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ₁₂] F) {C : ℝ},
  0 ≤ C → ∀ (h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖), ‖f.mkContinuous C h‖ ≤ C

If a continuous linear map is constructed from a linear map via the constructor mkContinuous, then its norm is bounded by the bound given to the constructor if it is nonnegative.

Defined in

Mathlib.Analysis.Normed.Operator.Basic

Cited by

16 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSeminormedAddCommGroupNontriviallyNormedFieldNontriviallyNormedFieldNormedSpaceNormedSpace