English
For any UpperSet s, the set {x ∈ M | mk x ∈ s} is a subsemigroup of M.
Русский
Для любого множества верхних элементов s множество {x ∈ M | mk x ∈ s} образует подполугруппу.
LaTeX
$$$\\{x \\in M \\mid \\\, \\operatorname{mk}(x) \\in s\\}$ образует подполугруппу М$$
Lean4
/-- Given a `UpperSet` of `MulArchimedeanClass`,
all group elements belonging to these classes form a subsemigroup.
This is not yet a subgroup because it doesn't contain the identity if `s = ⊤`. -/
@[to_additive /-- Given a `UpperSet` of `ArchimedeanClass`,
all group elements belonging to these classes form a subsemigroup.
This is not yet a subgroup because it doesn't contain the identity if `s = ⊤`. -/
]
def subsemigroup (s : UpperSet (MulArchimedeanClass M)) : Subsemigroup M
where
carrier := mk ⁻¹' s
mul_mem' {a b} ha
hb := by
rw [Set.mem_preimage] at ha hb ⊢
obtain h | h := min_le_iff.mp (min_le_mk_mul a b)
· exact s.upper h ha
· exact s.upper h hb
