instSeminormedAddCommGroup — Mathlib

English

The operator norm of f’s underlying continuous multilinear map equals the norm of f as a continuous alternating map.

Русский

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

LaTeX

$$$\|f.1\| = \|f\|$$$

Lean4

/-- Continuous alternating maps form a seminormed additive commutative group.
We override projection to `PseudoMetricSpace` to ensure that instances commute
in `with_reducible_and_instances`. -/
instance instSeminormedAddCommGroup : SeminormedAddCommGroup (E [⋀^ι]→L[𝕜] F)
    where
  toPseudoMetricSpace := .induced toContinuousMultilinearMap inferInstance
  __ := SeminormedAddCommGroup.induced _ _ (toMultilinearAddHom : E [⋀^ι]→L[𝕜] F →+ _)
  norm f := ‖f.toContinuousMultilinearMap‖

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