exists_minimal_closure_eq — Mathlib

English

If P is finitely generated, there exists a finite set S of generators such that P is the closure of S and S is minimal with this property.

Русский

Если P является конечнопорожденным, то существует конечный набор порождающих S, для которого P является замыканием S и который минимален по этому свойству.

LaTeX

$$$\\exists S : \\mathrm{Finset}\ M,\\ \\operatorname{Minimal}(\\operatorname{closure}(S.toSet) = P)\\ S$$$

Lean4

/-- A finitely generated submonoid has a minimal generating set. -/
@[to_additive /-- A finitely generated submonoid has a minimal generating set. -/
    ]
theorem exists_minimal_closure_eq (hP : P.FG) : ∃ S : Finset M, Minimal (closure ·.toSet = P) S :=
  exists_minimal_of_wellFoundedLT _ hP

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