continuousSMul

Mathlib.Topology.Algebra.MulAction

URI: https://scilib.ai/kg/mathlib#Subgroup.continuousSMul

English

The action of a subgroup S ≤ M on X is continuous.

Русский

Действие подгруппы S ⊆ M на X непрерывно.

LaTeX

$$ContinuousSMul (Subtype fun x => x ∈ S) X$$

Lean4

@[to_additive]
instance continuousSMul {S : Subgroup M} : ContinuousSMul S X :=
  S.toSubmonoid.continuousSMul

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru