English
Let H and K be submonoids of a monoid M. Then the join of H and K equals the closure of the product set {h k | h ∈ H, k ∈ K}. In particular, H ⊔ K = closure ((H : Set M) * (K : Set M)).
Русский
Пусть H и K — подмоноиды моноида M. Тогда объединение H и K равно замыканию множества произведений {h k | h ∈ H, k ∈ K}. То есть H ⊔ K = closure ((H : Set M) * (K : Set M)).
LaTeX
$$$H \\sqcup K = \\operatorname{closure}((H : \\mathrm{Set} M) \\cdot (K : \\mathrm{Set} M))$$$
Lean4
@[to_additive]
theorem sup_eq_closure_mul (H K : Submonoid M) : H ⊔ K = closure ((H : Set M) * (K : Set M)) :=
le_antisymm
(sup_le (fun h hh => subset_closure ⟨h, hh, 1, K.one_mem, mul_one h⟩) fun k hk =>
subset_closure ⟨1, H.one_mem, k, hk, one_mul k⟩)
((closure_mul_le _ _).trans <| by rw [closure_eq, closure_eq])
