isUniformEmbedding_equivBoundedOfCompact

English

The same equivalence (equivBoundedOfCompact α β) is a uniform embedding; in particular, it is injective and preserves the uniform structure.

Русский

Та же находимая эквиваленция (equivBoundedOfCompact α β) является равномерно вложением: она инъективна и сохраняет равномерную структуру.

LaTeX

$$$\mathrm{IsUniformEmbedding}\bigl(\mathrm{equivBoundedOfCompact}(\alpha,\beta)\bigr)$$$

Lean4

theorem isUniformEmbedding_equivBoundedOfCompact : IsUniformEmbedding (equivBoundedOfCompact α β) :=
  { isUniformInducing_equivBoundedOfCompact α β with injective := (equivBoundedOfCompact α β).injective }

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