continuousSubmodule — Mathlib

English

The set of all continuous maps α → M forms an R-submodule of the full function space α → M, i.e., a closed under addition and R-scalar multiplication subspace.

Русский

Множество всех непрерывных отображений α → M образует подмодуль над R в пространстве функций α → M, замкнутое относительно сложения и умножения на скаляры R.

LaTeX

$$$ \text{continuousSubmodule}(α,M) \subseteq R^{α} \text{ is a Submodule } R(α \to M). $$$

Lean4

/-- The `R`-submodule of continuous maps `α → M`. -/
def continuousSubmodule : Submodule R (α → M) :=
  { continuousAddSubgroup α M with
    carrier := {f : α → M | Continuous f}
    smul_mem' := fun c _ hf => hf.const_smul c }

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