uniformContinuous — Mathlib

English

The uniform continuity of a ContinuousAlgHom follows from its underlying additive structure when R-algebras are involved.

Русский

Единичная непрерывность по униформной топологии для ContinuousAlgHom следует из связанной структуры сложения в рамках R-алгебр.

LaTeX

$$$\\operatorname{uniformContinuous}~f$$$

Lean4

protected theorem uniformContinuous {E₁ E₂ : Type*} [UniformSpace E₁] [UniformSpace E₂] [Ring E₁] [Ring E₂]
    [Algebra R E₁] [Algebra R E₂] [IsUniformAddGroup E₁] [IsUniformAddGroup E₂] (f : E₁ →A[R] E₂) :
    UniformContinuous f :=
  uniformContinuous_addMonoidHom_of_continuous f.continuous

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