le_closure_toSubmonoid

Mathlib.Algebra.Group.Subgroup.Lattice

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

English

Submonoid.closure S ≤ (closure S).toSubmonoid.

Русский

Submonoid.closure S ≤ (closure S).toSubmonoid.

LaTeX

$$$ \\operatorname{Submonoid.closure}(S) \\le (\\mathrm{closure}(S)).\\text{toSubmonoid} $$$

Lean4

@[to_additive]
theorem le_closure_toSubmonoid (S : Set G) : Submonoid.closure S ≤ (closure S).toSubmonoid :=
  Submonoid.closure_le.2 subset_closure

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

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

Разделы

Аффилиация

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