Existence_of_Unique_Subsemigroup_Generated_by_Subset_v7
Provedgenerated-substructureproofwikisemigroupsubsemigroup
Let S be a monoid and X a subset of S. The submonoid generated by X is the smallest submonoid containing X.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Existence_of_Unique_Subsemigroup_Generated_by_Subset_v7 {S : Type _} [Monoid S] (X : Set S) (T : Submonoid S) (hXT : X ⊆ (T : Set S)) : Submonoid.closure X ≤ T := by sorrySource