instIsTopologicalAddGroup — Mathlib

English

The space of continuous alternating multilinear maps is itself a topological additive group; addition is continuous in the natural topology.

Русский

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

LaTeX

$$$\\text{IsTopologicalAddGroup}(\\operatorname{ContinuousAlternatingMap}_{𝕜} E F ι)$$$

Lean4

instance instIsTopologicalAddGroup : IsTopologicalAddGroup (E [⋀^ι]→L[𝕜] F) :=
  isEmbedding_toContinuousMultilinearMap.topologicalAddGroup (toContinuousMultilinearMapLinear (R := ℕ))

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