English
A refined version of the finite-index product formula under a technical nondegeneracy condition still yields the supremum decomposition.
Русский
Уточнённая версия формулы для конечного индекса с техническим условием даёт разложение на верхнюю грань (supremum).
LaTeX
$$$\\text{Under the stated technical conditions } egauge 𝕜(I.\\pi U) x = \\sup_{i∈I} egauge 𝕜(U_i)(x_i).$$$
Lean4
/-- The extended gauge of a point `x` in an indexed product
with respect to a product of finitely many balanced sets `U i`, `i ∈ I`,
(and the whole spaces for the other indices)
is the supremum of the extended gauges of the components of `x`
with respect to the corresponding balanced set.
This version assumes that `𝕜` is a nontrivially normed division ring.
See also `egauge_univ_pi` for when `s = univ`,
and `egauge_pi'` for a version with more choices of the technical assumptions.
-/
theorem egauge_pi [(𝓝[≠] (0 : 𝕜)).NeBot] {I : Set ι} {U : ∀ i, Set (E i)} (hI : I.Finite)
(hU : ∀ i ∈ I, Balanced 𝕜 (U i)) (x : ∀ i, E i) : egauge 𝕜 (I.pi U) x = ⨆ i ∈ I, egauge 𝕜 (U i) (x i) :=
egauge_pi' hI hU x <| .inr <| .inr inferInstance
