isUniformEmbedding — Mathlib

English

An algebra equivalence with continuous maps on both directions is a uniform embedding.

Русский

Алгебраическая эквивалентность с непрерывностью обеих направлений образует равномерно вложение.

LaTeX

$$$IsUniformEmbedding( e )$$$

Lean4

theorem _root_.AlgEquiv.isUniformEmbedding {E₁ E₂ : Type*} [UniformSpace E₁] [UniformSpace E₂] [Ring E₁]
    [IsUniformAddGroup E₁] [Algebra R E₁] [Ring E₂] [IsUniformAddGroup E₂] [Algebra R E₂] (e : E₁ ≃ₐ[R] E₂)
    (h₁ : Continuous e) (h₂ : Continuous e.symm) : IsUniformEmbedding e :=
  ContinuousAlgEquiv.isUniformEmbedding
    { e with
      continuous_toFun := h₁
      continuous_invFun := by dsimp; fun_prop }

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