isUniformInducing_coe — Mathlib

English

The canonical inclusion i: α → Completion α is an IsUniformInducing map, i.e., the uniform structure on α is induced by the inclusion from Completion α.

Русский

Каноническое включение i: α → Completion α является равномерно индуцирующим отображением; равномерная структура α индуцируется включением.

LaTeX

$$$\\mathrm{IsUniformInducing}(\\iota)\\;\\text{ where }\\iota:\\alpha \\to \\mathrm{Completion}(\\alpha)$$$

Lean4

theorem isUniformInducing_coe : IsUniformInducing ((↑) : α → Completion α) :=
  SeparationQuotient.isUniformInducing_mk.comp isUniformInducing_pureCauchy

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