smul_closure

Mathlib.Algebra.Group.Subgroup.Pointwise

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

English

The scalar action commutes with taking the closure of a set: a · closure(S) = closure(a · S).

Русский

Скалярное действие commuting с замыканием множества: a · closure(S) = closure(a · S).

LaTeX

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

Lean4

theorem smul_closure (a : α) (s : Set G) : a • closure s = closure (a • s) :=
  MonoidHom.map_closure _ _

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

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

Разделы

Аффилиация

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