English
For a finite index ι and a target algebra A with a normed structure, the norm of mkPiAlgebraFin 𝕜 ι A equals 1 when ι is nonempty and finite; in the empty case, it equals the norm of 1 in A. This shows how the Pi-construction interacts with the base norm.
Русский
Для конечного множества индексов ι и нормированного алгебраического пространства A норма mkPiAlgebraFin 𝕜 ι A равна 1, если ι непусто, и равна норме единицы в A в пустом случае.
LaTeX
$$$\|\mathrm{mkPiAlgebraFin}_{\mathbb{K}}(\iota, A)\| = 1$ (если ι непусто), и $\|\mathrm{mkPiAlgebraFin}_{\mathbb{K}}(\iota, A)\| = \|1\|$ (в пустом случае)$$
Lean4
@[simp]
theorem norm_mkPiAlgebra_le [Nonempty ι] : ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ ≤ 1 :=
by
refine opNorm_le_bound zero_le_one fun m => ?_
simp only [ContinuousMultilinearMap.mkPiAlgebra_apply, one_mul]
exact norm_prod_le' _ univ_nonempty _
