norm_mkPiAlgebra_of_empty — Mathlib

English

In the empty-index case, the operator norm of mkPiAlgebraFin 𝕜 ι A equals the norm of 1 in A, which is 1 if A has a unit. This provides a baseline for empty products.

Русский

В случае пустого индекса норма оператора mkPiAlgebraFin 𝕜 ι A равна норме 1 в A, что соответствует случаям, когда у A есть единица.

LaTeX

$$$\|\mathrm{mkPiAlgebraFin}_{\mathbb{K}}(\varnothing, A)\| = \|1\|$$$

Lean4

theorem norm_mkPiAlgebra_of_empty [IsEmpty ι] : ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ = ‖(1 : A)‖ :=
  by
  apply le_antisymm
  · apply opNorm_le_bound <;> simp
  · convert ratio_le_opNorm (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) fun _ => 1
    simp

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