English
If a continuous linear equivalence between uniform additive groups has continuous forward and inverse maps, then it is a uniform embedding.
Русский
Если непрерывное линейное биективное соответствие между равномерными группами имеет непрерывные переходы в обе стороны, то оно является равномерным вложением.
LaTeX
$$$IsUniformEmbedding(e)$$$
Lean4
protected theorem _root_.LinearEquiv.isUniformEmbedding {E₁ E₂ : Type*} [UniformSpace E₁] [UniformSpace E₂]
[AddCommGroup E₁] [AddCommGroup E₂] [Module R₁ E₁] [Module R₂ E₂] [IsUniformAddGroup E₁] [IsUniformAddGroup E₂]
(e : E₁ ≃ₛₗ[σ₁₂] E₂) (h₁ : Continuous e) (h₂ : Continuous e.symm) : IsUniformEmbedding e :=
ContinuousLinearEquiv.isUniformEmbedding
({ e with
continuous_toFun := h₁
continuous_invFun := h₂ } :
E₁ ≃SL[σ₁₂] E₂)
