isUniformEmbedding — Mathlib

English

Any continuous algebra equivalence between uniform spaces is a uniform embedding.

Русский

Любое непрерывное алгебраическое эквивалентное отображение между равномерными пространствами является равномерно вложенным отображением.

LaTeX

$$$IsUniformEmbedding\ e$$$

Lean4

theorem isUniformEmbedding {E₁ E₂ : Type*} [UniformSpace E₁] [UniformSpace E₂] [Ring E₁] [IsUniformAddGroup E₁]
    [Algebra R E₁] [Ring E₂] [IsUniformAddGroup E₂] [Algebra R E₂] (e : E₁ ≃A[R] E₂) : IsUniformEmbedding e :=
  e.toAlgEquiv.isUniformEmbedding e.toContinuousAlgHom.uniformContinuous e.symm.toContinuousAlgHom.uniformContinuous

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