commSemigroup — Mathlib

English

Under the product S * T = { xy | x ∈ S, y ∈ T }, the collection of upper sets forms a commutative semigroup.

Русский

При произведении S * T = { xy | x ∈ S, y ∈ T } множество верхних множеств образует коммутативную полугруппу.

LaTeX

$$UpperSet α is a CommSemigroup under the product S * T := { xy : x ∈ S, y ∈ T }.$$

Lean4

@[to_additive]
instance commSemigroup : CommSemigroup (UpperSet α) :=
  { (SetLike.coe_injective.commSemigroup _ coe_mul : CommSemigroup (UpperSet α)) with }

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