English
The uniformity on α ⊕ β is given by the explicit map-sup formula described earlier.
Русский
Равномерность на α ⊕ β задаётся явной формулой отображения как супремуп прилежащих равномерностей из α и β.
LaTeX
$$$\\mathcal{U}(α \\oplus β) = \\operatorname{map}(\\operatorname{Prod.map} (\\mathrm{inl}, \\mathrm{inl}))(\\mathcal{U}(α)) \\;⊔\\; \\operatorname{map}(\\operatorname{Prod.map}(\\mathrm{inr}, \\mathrm{inr}))(\\mathcal{U}(β))$$$
Lean4
/-- Uniformity on a disjoint union. Entourages of the diagonal in the union are obtained
by taking independently an entourage of the diagonal in the first part, and an entourage of
the diagonal in the second part. -/
instance instUniformSpace : UniformSpace (α ⊕ β)
where
uniformity := map (fun p : α × α => (inl p.1, inl p.2)) (𝓤 α) ⊔ map (fun p : β × β => (inr p.1, inr p.2)) (𝓤 β)
symm := fun _ hs ↦ ⟨symm_le_uniformity hs.1, symm_le_uniformity hs.2⟩
comp := fun s hs ↦ by
rcases comp_mem_uniformity_sets hs.1 with ⟨tα, htα, Htα⟩
rcases comp_mem_uniformity_sets hs.2 with ⟨tβ, htβ, Htβ⟩
filter_upwards [mem_lift' (union_mem_sup (image_mem_map htα) (image_mem_map htβ))]
rintro ⟨_, _⟩ ⟨z, ⟨⟨a, b⟩, hab, ⟨⟩⟩ | ⟨⟨a, b⟩, hab, ⟨⟩⟩, ⟨⟨_, c⟩, hbc, ⟨⟩⟩ | ⟨⟨_, c⟩, hbc, ⟨⟩⟩⟩
exacts [@Htα (_, _) ⟨b, hab, hbc⟩, @Htβ (_, _) ⟨b, hab, hbc⟩]
nhds_eq_comap_uniformity
x := by
ext
cases x <;> simp [mem_comap', -mem_comap, nhds_inl, nhds_inr, nhds_eq_comap_uniformity, Prod.ext_iff]
