English
There is a natural uniform structure on the disjoint union α ⊕ β, defined so that its uniformity is the supremum of the pushforwards of 𝓤 α and 𝓤 β along the injections inl and inr.
Русский
Для непересекаемого объединения α ⊕ β существует естественная равномерная структура, чья равномерность равна наивысшему пределу образов 𝓤 α и 𝓤 β по инъекциям inl и inr.
LaTeX
$$$\\mathcal{U}(α \\oplus β) = \\operatorname{map}(\\operatorname{Prod.map} (\\mathrm{inl}, \\mathrm{inl}))(\\mathcal{U}(α)) \\;\\sqcup\\; \\operatorname{map}(\\operatorname{Prod.map}(\\mathrm{inr}, \\mathrm{inr}))(\\mathcal{U}(β))$$$
Lean4
theorem toTopologicalSpace_subtype [u : UniformSpace α] {p : α → Prop} :
@UniformSpace.toTopologicalSpace (Subtype p) instUniformSpaceSubtype =
@instTopologicalSpaceSubtype α p u.toTopologicalSpace :=
rfl
