mul_subset

Mathlib.Algebra.Group.Submonoid.Pointwise

URI: https://scilib.ai/kg/mathlib#Submonoid.mul_subset

← MathLib Explorer

English

If s ⊆ S and t ⊆ S for a submonoid S of a monoid M, then the product set s * t is contained in S.

Русский

Если s, t подмножества внутри S, то их произведение лежит в S.

LaTeX

$$$ s * t \subseteq S $ given s \subseteq S \ and\ t \subseteq S $$$

Lean4

@[to_additive]
theorem mul_subset {S : Submonoid M} (hs : s ⊆ S) (ht : t ⊆ S) : s * t ⊆ S :=
  mul_subset_iff.2 fun _x hx _y hy ↦ mul_mem (hs hx) (ht hy)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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