continuousSMul — Mathlib

English

Let F be a topological division ring and M ≤ F a subfield. Then the induced scalar action of M on any space X with a continuous F-action is continuous; i.e., the restricted action is continuous.

Русский

Пусть F — топологическое делимое кольцо, M ≤ F подполе. Тогда ограниченное скалярное умножение M на X является непрерывным, если исходное действие F на X непрерывно.

LaTeX

$$ContinuousSMul M X$$

Lean4

instance continuousSMul (M : Subfield F) : ContinuousSMul M X :=
  Subring.continuousSMul M.toSubring X

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