English
The uniformity on the subset {x ∈ α | p x} is the comap of 𝓤 α along the inclusion map.
Русский
Равномерность подмножества {x ∈ α | p x} равна композиции обратной проекции по включению в α.
LaTeX
$$$$\\mathcal{U}(\\mathrm{Subtype}(p)) = \\mathrm{comap}\\big( (\\lambda q:\\mathrm{Subtype}(p) \\times \\mathrm{Subtype}(p), (q.1.1, q.2.1)) \\big)\\, \\mathcal{U}(\\alpha).$$$$
Lean4
theorem uniformity_subtype {p : α → Prop} [UniformSpace α] :
𝓤 (Subtype p) = comap (fun q : Subtype p × Subtype p => (q.1.1, q.2.1)) (𝓤 α) :=
rfl