English
If α is a semigroup, then Filter α is a semigroup under pointwise multiplication; associativity holds: (f * g) * h = f * (g * h).
Русский
Если α — полугруппа, то Filter α образует полугруппу под точечным умножением; ассоциативность выполняется: (f * g) * h = f * (g * h).
LaTeX
$$$\forall f,g,h \in \mathrm{Filter}(\alpha),\ (f * g) * h = f * (g * h).$$$
Lean4
/-- `Filter α` is a `Semigroup` under pointwise operations if `α` is. -/
@[to_additive /-- `Filter α` is an `AddSemigroup` under pointwise operations if `α` is. -/
]
protected def semigroup [Semigroup α] : Semigroup (Filter α)
where
mul := (· * ·)
mul_assoc _ _ _ := map₂_assoc mul_assoc
