English
For any UpperSet s, the subgroup associated to s extends the subsemigroup when s ≠ ⊤, with the identity and inverses included accordingly.
Русский
Для любого верхнего множества s сопряженная к нему подгруппа расширяет соответствующую подполугруппу при условии s ≠ ⊤, включая единицу и обратные элементы.
LaTeX
$$$\\text{If } s \\neq \\top, \\ \\text{subgroup}(s) \\text{ is the subgroup generated by } \\{x \\mid mk(x) \\in s\\}$$$
Lean4
/-- Make `MulArchimedeanClass.subsemigroup` a subgroup by assigning
s = ⊤ with a junk value ⊥. -/
@[to_additive /-- Make `ArchimedeanClass.subsemigroup` a subgroup by assigning
s = ⊤ with a junk value ⊥. -/
]
noncomputable def subgroup (s : UpperSet (MulArchimedeanClass M)) : Subgroup M :=
open Classical in
if hs : s = ⊤ then ⊥
else
{
subsemigroup
s with
one_mem' := by
rw [subsemigroup, Set.mem_preimage]
obtain ⟨u, hu⟩ := UpperSet.coe_nonempty.mpr hs
simpa using s.upper (by simp) hu
inv_mem' := by simp [subsemigroup] }
