dist_algebraMap' — Mathlib

English

The product of finitely many normed algebras, indexed by a finite set, is a normed algebra with the sup norm.

Русский

Произведение конечного числа нормированных алгебр по индексу конечного множества является нормированной алгеброй с суп-нормой.

LaTeX

$$$\\mathrm{NormedAlgebra}_{\\mathbb{K}}\\big(\\prod_{i=1}^n E_i\\big)$$$

Lean4

/-- This is a simpler version of `dist_algebraMap` when `‖1‖ = 1` in `𝕜'`. -/
@[simp]
theorem dist_algebraMap' [NormOneClass 𝕜'] (x y : 𝕜) : (dist (algebraMap 𝕜 𝕜' x) (algebraMap 𝕜 𝕜' y)) = dist x y := by
  simp only [dist_eq_norm, ← map_sub, norm_algebraMap']

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