Theorems · Theorem · functional analysis

ContinuousLinearMap.opNorm_extend_le

∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedAddCommGroup Eₗ] [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 E]
  [inst_6 : NormedSpace 𝕜 Eₗ] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : CompleteSpace F] (f : E →SL[σ₁₂] F) {e : E →L[𝕜] Eₗ}
  {N : NNReal} [RingHomIsometric σ₁₂], DenseRange ⇑e → (∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖) → ‖f.extend e‖ ≤ ↑N * ‖f‖

If a dense embedding e : E →L[𝕜] G expands the norm by a constant factor N⁻¹, then the norm of the extension of f along e is bounded by N * ‖f‖.

Defined in

Mathlib.Analysis.Normed.Operator.Extend

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNontriviallyNormedFieldNormedAddCommGroupNormedAddCommGroupNormedAddCommGroupNormedSpaceNormedSpaceNormedSpaceCompleteSpaceRingHomIsometric