uniformity_subtype — Mathlib

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

Похожие утверждения