uniformContinuous — Mathlib

English

A continuous σ12-semilinear map between uniform additive groups is uniformly continuous.

Русский

Непрерывное σ12-семилинейное отображение между униформными аддитивными группами является равномерно непрерывным.

LaTeX

$$$f: E_1 \toSL[\sigma_{12}] E_2\quad\Rightarrow\quad f\text{ uniformly continuous}$$$

Lean4

protected theorem uniformContinuous {E₁ E₂ : Type*} [UniformSpace E₁] [UniformSpace E₂] [AddCommGroup E₁]
    [AddCommGroup E₂] [Module R₁ E₁] [Module R₂ E₂] [IsUniformAddGroup E₁] [IsUniformAddGroup E₂] (f : E₁ →SL[σ₁₂] E₂) :
    UniformContinuous f :=
  uniformContinuous_addMonoidHom_of_continuous f.continuous

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