instContinuousSMul — Mathlib

English

If α has a topological structure and a continuous ℂ-action, then Circle acts continuously on α.

Русский

Если имеется топологическое пространство на α и непрерывное действие ℂ на α, то Circle действует непрерывно на α.

LaTeX

$$$$ \\text{ContinuousSMul Circle } \\alpha. $$$$

Lean4

instance instContinuousSMul [TopologicalSpace α] [MulAction ℂ α] [ContinuousSMul ℂ α] : ContinuousSMul Circle α :=
  Submonoid.continuousSMul

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