isBoundedBilinearMap_comp — Mathlib

English

The map sending (g, f) to g ∘ f, where g ∈ (F →L G) and f ∈ (E →L F), is a bounded bilinear map.

Русский

Отображение, отправляющее (g,f) ↦ g ∘ f, где g ∈ (F →L G), f ∈ (E →L F), является ограниченным билинейным отображением.

LaTeX

$$$IsBoundedBilinearMap 𝕜 \bigl(p \mapsto p.1 \circ p.2\bigr)$$$

Lean4

theorem isBoundedBilinearMap_comp : IsBoundedBilinearMap 𝕜 fun p : (F →L[𝕜] G) × (E →L[𝕜] F) => p.1.comp p.2 :=
  (compL 𝕜 E F G).isBoundedBilinearMap

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