English
If ι is finite and each U_i is balanced, the gauge on the universal product equals the supremum of the component gauges.
Русский
Для конечного индекса ι и сбалансированных U_i верно: egauge(универсальный произведение) = sup egauge(U_i)(x_i).
LaTeX
$$$\\forall ι, E_i,\\; \\text{Finite } ι \\;\\Rightarrow\\; egauge 𝕜 (\\text{univ.pi } U) x = \\sup_i egauge 𝕜 (U_i)(x_i).$$$
Lean4
/-- A set `B` is exposed with respect to `A` iff it maximizes some functional over `A` (and contains
all points maximizing it). Written `IsExposed 𝕜 A B`. -/
def IsExposed (A B : Set E) : Prop :=
B.Nonempty → ∃ l : StrongDual 𝕜 E, B = {x ∈ A | ∀ y ∈ A, l y ≤ l x}
