isBoundedBilinearMap_apply — Mathlib

English

For f ∈ E →L F, the map g ↦ g ∘ f is a bounded linear map from F →L G to G.

Русский

Для f ∈ E →L F отображение g ↦ g ∘ f является ограниченным линейным отображением от F →L G в G.

LaTeX

$$$IsBoundedLinearMap 𝕜 (\lambda g: F →L[𝕜] G, g.comp f)$$$

Lean4

theorem isBoundedBilinearMap_apply : IsBoundedBilinearMap 𝕜 fun p : (E →L[𝕜] F) × E => p.1 p.2 :=
  (ContinuousLinearMap.flip (apply 𝕜 F : E →L[𝕜] (E →L[𝕜] F) →L[𝕜] F)).isBoundedBilinearMap

Похожие утверждения