English
The submonoid generated by a set is the smallest submonoid containing that set; it is defined as the intersection of all submonoids containing the set.
Русский
Подмножество, порождаемое набором, есть наименьшее подпомонид, содержащий этот набор; определено как пересечение всех подпmonoid, содержащих набор.
LaTeX
$$closure(s) = ⋂{ S ⊆ M | S является Submonoid и s ⊆ S }$$
Lean4
/-- Submonoids of a monoid form a complete lattice. -/
@[to_additive /-- The `AddSubmonoid`s of an `AddMonoid` form a complete lattice. -/
]
instance : CompleteLattice (Submonoid M) :=
{
(completeLatticeOfInf (Submonoid M)) fun _ =>
IsGLB.of_image (f := (SetLike.coe : Submonoid M → Set M))
(@fun S T => show (S : Set M) ≤ T ↔ S ≤ T from SetLike.coe_subset_coe)
isGLB_biInf with
le := (· ≤ ·)
lt := (· < ·)
bot := ⊥
bot_le := fun S _ hx => (mem_bot.1 hx).symm ▸ S.one_mem
top := ⊤
le_top := fun _ x _ => mem_top x
inf := (· ⊓ ·)
sInf := InfSet.sInf
le_inf := fun _ _ _ ha hb _ hx => ⟨ha hx, hb hx⟩
inf_le_left := fun _ _ _ => And.left
inf_le_right := fun _ _ _ => And.right }
