mkContinuous_norm_le' — Mathlib

English

The prime version of mkContinuous_norm_le' gives an upper bound by the maximum of C and 0.

Русский

Прайм-версия mkContinuous_norm_le' даёт верхнюю границу максимумом C и нуль.

LaTeX

$$$\|f^{\mathrm{mkContinuous}}\| \le \max\{C,0\}$$$

Lean4

/-- If a continuous alternating map is constructed from a alternating map via the constructor
`mk_continuous`, then its norm is bounded by the bound given to the constructor if it is
nonnegative. -/
theorem mkContinuous_norm_le' (f : E [⋀^ι]→ₗ[𝕜] F) {C : ℝ} (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) :
    ‖f.mkContinuous C H‖ ≤ max C 0 :=
  ContinuousMultilinearMap.opNorm_le_bound (le_max_right _ _) fun m ↦
    (H m).trans <| by
      gcongr
      apply le_max_left

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