smul_closure — Mathlib

English

Let a act on M via aMul action, and S be a subset of M. Then the action commutes with taking the submonoid closure: a · closure(S) = closure(a · S).

Русский

Пусть действует действие α на моноид M, и S подмножество M. Тогда изображение через действие отобразит замыкание подмоноида: a · closure(S) = closure(a · S).

LaTeX

$$$a \\cdot \\operatorname{closure}(S) = \\operatorname{closure}(a \\cdot S)$$$

Lean4

theorem smul_closure (a : α) (s : Set M) : a • closure s = closure (a • s) :=
  MonoidHom.map_mclosure _ _

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