English
The uniformity on SeparationQuotient α is the pushforward of the uniformity on α by the map mk.
Русский
Равномерность на SeparationQuotient α равна образованию равномерности через отображение mk.
LaTeX
$$$𝓤(SeparationQuotient(α)) = 𝓤(α).map (Prod.map mk mk)$$$
Lean4
instance instUniformSpace : UniformSpace (SeparationQuotient α)
where
uniformity := map (Prod.map mk mk) (𝓤 α)
symm := tendsto_map' <| tendsto_map.comp tendsto_swap_uniformity
comp := fun t ht ↦ by
rcases comp_open_symm_mem_uniformity_sets ht with ⟨U, hU, hUo, -, hUt⟩
refine mem_of_superset (mem_lift' <| image_mem_map hU) ?_
simp only [subset_def, Prod.forall, mem_compRel, mem_image, Prod.ext_iff]
rintro _ _ ⟨_, ⟨⟨x, y⟩, hxyU, rfl, rfl⟩, ⟨⟨y', z⟩, hyzU, hy, rfl⟩⟩
have : y' ⤳ y := (mk_eq_mk.1 hy).specializes
exact @hUt (x, z) ⟨y', this.mem_open (UniformSpace.isOpen_ball _ hUo) hxyU, hyzU⟩
nhds_eq_comap_uniformity :=
surjective_mk.forall.2 fun x ↦
comap_injective surjective_mk <|
by
conv_lhs => rw [comap_mk_nhds_mk, nhds_eq_comap_uniformity, ← comap_map_mk_uniformity]
simp only [Filter.comap_comap, Function.comp_def, Prod.map_apply]
