mul_mem — Mathlib

English

A subsemigroup is closed under multiplication: if x,y ∈ S then x y ∈ S.

Русский

Подполугруппа замкнута относительно умножения: если x,y ∈ S, то xy ∈ S.

LaTeX

$$$ \forall x,y \in S, \\; x y \\in S $$$

Lean4

/-- A subsemigroup is closed under multiplication. -/
@[to_additive /-- An `AddSubsemigroup` is closed under addition. -/
    ]
protected theorem mul_mem {x y : M} : x ∈ S → y ∈ S → x * y ∈ S :=
  Subsemigroup.mul_mem' S

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