English
The uniformity on the sum α ⊕ β is equal to the supremum of the pushforwards of 𝓤 α and 𝓤 β via the injections.
Русский
Равномерность пространства суммы α ⊕ β равна верхней границе образов 𝓤 α и 𝓤 β через инъекции.
LaTeX
$$$\\mathcal{U}(\\alpha \\oplus \\beta) = \\operatorname{map}(\\operatorname{Prod.map} (\\mathrm{inl}, \\mathrm{inl}))(\\mathcal{U}(\\alpha)) \\;⊔\\; \\operatorname{map}(\\operatorname{Prod.map}(\\mathrm{inr}, \\mathrm{inr}))(\\mathcal{U}(\\beta))$$$
Lean4
/-- The union of an entourage of the diagonal in each set of a disjoint union is again an entourage
of the diagonal. -/
theorem union_mem_uniformity_sum {a : Set (α × α)} (ha : a ∈ 𝓤 α) {b : Set (β × β)} (hb : b ∈ 𝓤 β) :
Prod.map inl inl '' a ∪ Prod.map inr inr '' b ∈ 𝓤 (α ⊕ β) :=
union_mem_sup (image_mem_map ha) (image_mem_map hb)
