English
If M is a commutative monoid with a partial order and the Archimedean property, then any submonoid H (viewed as a substructure) inherits the Archimedean property with respect to the ambient order; in particular, H is MulArchimedean.
Русский
Пусть M — коммутативная моноида с частичным порядком и Архимедовым свойством; любая подмоноида H наследует это свойство (с точностью до порядка), то есть H является MulArchimedean.
LaTeX
$$$H\\subseteq M\\quad\\Rightarrow\\quad MulArchimedean(H)$$$
Lean4
@[to_additive]
instance instMulArchimedean {M S : Type*} [SetLike S M] [CommMonoid M] [PartialOrder M] [SubmonoidClass S M]
[MulArchimedean M] (H : S) : MulArchimedean H := by
constructor
rintro x _
simp only [← Subtype.coe_lt_coe, OneMemClass.coe_one]
exact MulArchimedean.arch x.val
