English
Let E1 and E2 be uniform spaces that are also additive groups with compatible module structures. If e: E1 → E2 is a continuous linear equivalence (with a continuous inverse), then e is a uniform embedding; i.e., e is an injective uniform map whose image carries the subspace uniform structure from E2.
Русский
Пусть E1 и E2 — униформные пространства, являющиеся аддитивными группами с совместимой надмодулярной структурой. Если e: E1 → E2 — непрерывное линейное биекция и обратное отображение также непрерывно, то e является равномерным вложением; то есть отображение инъективное и образ несет подпространственную равномерную структуру пространства E2.
LaTeX
$$$IsUniformEmbedding\\ (e)$$$
Lean4
theorem isUniformEmbedding {E₁ E₂ : Type*} [UniformSpace E₁] [UniformSpace E₂] [AddCommGroup E₁] [AddCommGroup E₂]
[Module R₁ E₁] [Module R₂ E₂] [IsUniformAddGroup E₁] [IsUniformAddGroup E₂] (e : E₁ ≃SL[σ₁₂] E₂) :
IsUniformEmbedding e :=
e.toLinearEquiv.toEquiv.isUniformEmbedding e.toContinuousLinearMap.uniformContinuous
e.symm.toContinuousLinearMap.uniformContinuous
