English
If M acts on N and N acts on α with a scalar tower structure, and all relevant smuls are continuous, then M acts continuously on α.
Русский
Пусть M действует на N, N действует на α и существует структура IsScalarTower; при условии непрерывности всех сопутствующих действий, M действует непрерывно на α.
LaTeX
$$$\\text{ContinuousSMul } M α$ under IsScalarTower M N α given appropriate continuity assumptions$$
Lean4
theorem continuousSMul {M : Type*} (N : Type*) {α : Type*} [Monoid N] [SMul M N] [MulAction N α] [SMul M α]
[IsScalarTower M N α] [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace α] [ContinuousSMul M N]
[ContinuousSMul N α] : ContinuousSMul M α :=
{
continuous_smul := by
suffices Continuous (fun p : M × α ↦ (p.1 • (1 : N)) • p.2) by simpa
fun_prop }
