uniformity_setCoe — Mathlib

English

The uniformity on a subset s ⊆ α is the comap of the inclusion map from s to α.

Русский

Равномерность множества s ⊆ α равна композиции обратной по включению s ↪ α.

LaTeX

$$$$\\mathcal{U}(s) = \\mathrm{comap}\\big( (\\uparrow) : s \\to \\alpha \\big) (\\mathcal{U}(\\alpha)).$$$$

Lean4

theorem uniformity_setCoe {s : Set α} [UniformSpace α] : 𝓤 s = comap (Prod.map ((↑) : s → α) ((↑) : s → α)) (𝓤 α) :=
  rfl

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