instNormedAddCommGroup — Mathlib

English

The space of continuous alternating maps E [⋀^ι]→ L[𝕜] F forms a normed additive commutative group with respect to the operator norm.

Русский

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

LaTeX

$$$\\text{ContinuousAlternatingMap}(\\,\\cdot\\,):= (E [⋀^ι]→L[𝕜] F) \\text{ is a } \\|\\cdot\\|\\text{-normed additive commutative group}$$$

Lean4

/-- Continuous alternating maps themselves form a normed group with respect to the operator norm. -/
instance instNormedAddCommGroup : NormedAddCommGroup (E [⋀^ι]→L[𝕜] F) :=
  NormedAddCommGroup.ofSeparation fun _f hf ↦ toContinuousMultilinearMap_injective <| norm_eq_zero.mp hf

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