English
Under the same finiteness and balance hypotheses, egauge on the indexed product equals the supremum over i in I of egauge on each component.
Русский
При тех же предположениях верна та же формула: egauge 𝕜 (I.π U) x = ⨆ i∈I, egauge 𝕜 (U_i) (x_i).
LaTeX
$$$\\forall 𝕜\\,[\\text{NormedDivisionRing } 𝕜],\\; \\forall I, U, x:\\; I.Finite → (\\forall i∈I, Balanced 𝕜 (U_i)) → egauge_{\\mathbb{k}}(I.\\pi U, x) = \\sup_{i∈I} egauge_{\\mathbb{k}}(U_i)(x_i).$$$
Lean4
/-- The extended gauge of a point `x` in an indexed product with finite index type
with respect to a product of balanced sets `U i`,
is the supremum of the extended gauges of the components of `x`
with respect to the corresponding balanced set.
-/
theorem egauge_univ_pi [Finite ι] {U : ∀ i, Set (E i)} (hU : ∀ i, Balanced 𝕜 (U i)) (x : ∀ i, E i) :
egauge 𝕜 (univ.pi U) x = ⨆ i, egauge 𝕜 (U i) (x i) :=
egauge_pi' finite_univ (fun i _ ↦ hU i) x (.inl rfl) |>.trans <| by simp
