balancedHull — Mathlib

English

The balanced hull can be expressed as the union of scaled copies of s over scalars with norm ≤ 1.

Русский

Балансированная оболочка равняется объединению масштабированных копий s на скалярах с нормой ≤ 1.

LaTeX

$$$\\operatorname{balancedHull}_{\\mathbb{R}}(s) = \\bigcup_{r: \\mathbb{K},\\ ||r||\\le 1} r \\cdot s$$$

Lean4

/-- The smallest balanced superset of `s`. -/
def balancedHull (s : Set E) :=
  ⋃ (r : 𝕜) (_ : ‖r‖ ≤ 1), r • s

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