English
For balanced sets U in E and V in F, the gauge of the product set U×V at (a,b) equals the maximum of the gauges of a and b with respect to U and V respectively.
Русский
Для сбалансированных множеств U⊆E и V⊆F верно: egauge 𝕜 (U×V) (a,b) = max(egauge 𝕜 U a, egauge 𝕜 V b).
LaTeX
$$$\\forall 𝕜\\,[\\text{NormedDivisionRing } 𝕜],\\; \\forall E,F,\\; \\forall U\\subseteq E, V\\subseteq F,\\; \\text{Balanced } 𝕜 U,\\; \\text{Balanced } 𝕜 V:\\; \\operatorname{egauge}_{\\mathbb{k}}(U\\times V, (a,b)) = \\max\\big( \\operatorname{egauge}_{\\mathbb{k}}(U,a), \\operatorname{egauge}_{\\mathbb{k}}(V,b) \\big).$$$
Lean4
/-- The extended gauge of a point `(a, b)` with respect to the product of balanced sets `U` and `V`
is equal to the maximum of the extended gauges of `a` with respect to `U`
and `b` with respect to `V`.
-/
theorem egauge_prod_mk {F : Type*} [AddCommGroup F] [Module 𝕜 F] {U : Set E} {V : Set F} (hU : Balanced 𝕜 U)
(hV : Balanced 𝕜 V) (a : E) (b : F) : egauge 𝕜 (U ×ˢ V) (a, b) = max (egauge 𝕜 U a) (egauge 𝕜 V b) :=
by
refine le_antisymm (le_of_forall_gt fun r hr ↦ ?_) (le_egauge_prod _ _ _ _)
simp only [max_lt_iff, egauge_lt_iff, smul_set_prod] at hr ⊢
rcases hr with ⟨⟨x, hx, hxr⟩, ⟨y, hy, hyr⟩⟩
cases le_total ‖x‖ ‖y‖ with
| inl hle => exact ⟨y, ⟨hU.smul_mono hle hx, hy⟩, hyr⟩
| inr hle => exact ⟨x, ⟨hx, hV.smul_mono hle hy⟩, hxr⟩
