mkContinuous₂_norm_le' — Mathlib

English

There exists a bound for the norm of mkContinuous₂ built from a bilinear map, with a bound derived from C and input norms.

Русский

Существует ограничение нормы mkContinuous₂, выведенное из константы C и норм входов.

LaTeX

$$$ \|f.mkContinuous₂ C hC\| \le \max\{C,0\} $$$

Lean4

theorem mkContinuous₂_norm_le' (f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) {C : ℝ} (hC : ∀ x y, ‖f x y‖ ≤ C * ‖x‖ * ‖y‖) :
    ‖f.mkContinuous₂ C hC‖ ≤ max C 0 :=
  mkContinuous_norm_le _ (le_max_iff.2 <| Or.inr le_rfl) (norm_mkContinuous₂_aux f C hC)

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