English
The submonoid closure of a set is the union of {1} and the subsemigroup closure of the set.
Русский
Замыкание подпол мон может быть представлено как объединение {1} и замыкания подполю полусупом.
LaTeX
$$closure s = {1} ∪ (Subsemigroup.closure s : Set M)$$
Lean4
/-- The `Submonoid.closure` of a set is the union of `{1}` and its `Subsemigroup.closure`. -/
theorem closure_eq_one_union (s : Set M) : closure s = {(1 : M)} ∪ (Subsemigroup.closure s : Set M) :=
by
apply le_antisymm
· intro x hx
induction hx using closure_induction with
| mem x hx => exact Or.inr <| Subsemigroup.subset_closure hx
| one => exact Or.inl <| by simp
| mul x hx y hy hx hy =>
simp only [singleton_union, mem_insert_iff, SetLike.mem_coe] at hx hy
obtain ⟨(rfl | hx), (rfl | hy)⟩ := And.intro hx hy
all_goals simp_all
exact Or.inr <| mul_mem hx hy
· rintro x (hx | hx)
· exact (show x = 1 by simpa using hx) ▸ one_mem (closure s)
· exact Subsemigroup.closure_le.mpr subset_closure hx
