exists_minimal_closure_eq_top — Mathlib

English

If a submonoid is finitely generated, then there exists a minimal generating set with closure equal to top.

Русский

Если под-монойд конечнопорожден, то существует минимальный набор порождения с замыканием равным ⊤.

LaTeX

$$$\\exists S : Finset M, Minimal (\\lambda s, Eq (Submonoid.closure s.toSet) ⊤) S$$$

Lean4

/-- A finitely generated monoid has a minimal generating set. -/
@[to_additive /-- A finitely generated monoid has a minimal generating set. -/
    ]
theorem exists_minimal_closure_eq_top [Monoid.FG M] : ∃ S : Finset M, Minimal (Submonoid.closure ·.toSet = ⊤) S :=
  Monoid.FG.fg_top.exists_minimal_closure_eq

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