bound — Mathlib

English

Continuous alternating maps form a seminormed additive commutative group under the induced structure.

Русский

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

LaTeX

$$$\text{SeminormedAddCommGroup}(\text{ContinuousAlternatingMap } 𝕜 E F ι)$$$

Lean4

theorem bound (f : E [⋀^ι]→L[𝕜] F) : ∃ (C : ℝ), 0 < C ∧ (∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) :=
  f.toContinuousMultilinearMap.bound

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