English
If U,V are balanced subsets of E, then egauge on U+V at a+b is at most the maximum of egauge on U at a and on V at b.
Русский
Если U,V сбалансированы, то egauge 𝕜 (U+V) (a+b) ≤ max(egauge 𝕜 U a, egauge 𝕜 V b).
LaTeX
$$$\\forall 𝕜\\,[\\text{NormedDivisionRing } 𝕜],\\; \\forall U,V\\subseteq E,\\; \\text{Balanced } 𝕜 U,\\; \\text{Balanced } 𝕜 V:\\; \\operatorname{egauge}_{\\mathbb{k}}(U+V, a+b) \\le \\max\\big( \\operatorname{egauge}_{\\mathbb{k}}(U,a), \\operatorname{egauge}_{\\mathbb{k}}(V,b) \\big).$$$
Lean4
theorem egauge_add_add_le {U V : Set E} (hU : Balanced 𝕜 U) (hV : Balanced 𝕜 V) (a b : E) :
egauge 𝕜 (U + V) (a + b) ≤ max (egauge 𝕜 U a) (egauge 𝕜 V b) :=
by
rw [← egauge_prod_mk hU hV a b, ← add_image_prod]
exact MapsTo.egauge_le 𝕜 (LinearMap.fst 𝕜 E E + LinearMap.snd 𝕜 E E) (mapsTo_image _ _) (a, b)
