English
Precomposition by a continuous map never increases the norm of a bounded map.
Русский
Пре-композиция непрерывной отображения никогда не увеличивает норму ограниченного отображения.
LaTeX
$$$‖f.compContinuous g‖ ≤ ‖f‖$$$
Lean4
/-- Postcomposition of bounded continuous functions into a normed module by a continuous linear map
is a continuous linear map.
Upgraded version of `ContinuousLinearMap.compLeftContinuous`, similar to `LinearMap.compLeft`. -/
protected def _root_.ContinuousLinearMap.compLeftContinuousBounded (g : β →L[𝕜] γ) : (α →ᵇ β) →L[𝕜] α →ᵇ γ :=
LinearMap.mkContinuous
{ toFun := fun f =>
ofNormedAddCommGroup (g ∘ f) (g.continuous.comp f.continuous) (‖g‖ * ‖f‖) fun x =>
g.le_opNorm_of_le (f.norm_coe_le_norm x)
map_add' := fun f g => by ext; simp
map_smul' := fun c f => by ext; simp } ‖g‖ fun f =>
norm_ofNormedAddCommGroup_le _ (mul_nonneg (norm_nonneg g) (norm_nonneg f))
(fun x => by exact g.le_opNorm_of_le (f.norm_coe_le_norm x))
