nnnorm_ofSubsingleton_id — Mathlib

English

The operation space of continuous alternating maps is a normed additive commutative group under the operator norm.

Русский

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

LaTeX

$$$\\text{NormedAddCommGroup}(\\text{ContinuousAlternatingMap } (E, F))$$$

Lean4

theorem nnnorm_ofSubsingleton_id [Subsingleton ι] [Nontrivial F] (i : ι) : ‖ofSubsingleton 𝕜 F F i (.id _ _)‖₊ = 1 :=
  NNReal.eq <| norm_ofSubsingleton_id ..

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