English
If there is a strictly monotone monoid homomorphism f from G into a MulArchimedean M, then G is MulArchimedean; i.e., Archimedeanness is inherited along order-preserving monoid homomorphisms.
Русский
Если существует строго монотонная гомоморфная карта f: G→M между моноидами, где M обладает Архимедовым свойством, то G также обладает Архимедовым свойством; то есть Архимедовость сохраняется под сохраняющей порядок моноидеобразующей.
LaTeX
$$$\\forall f: G \\to M\\, (\\text{MonoidHom } f)\\, \\forall hf: \\text{StrictMono}(f)\\;\\Rightarrow\\; \\text{MulArchimedean}(G).$$$
Lean4
@[to_additive]
theorem comap [CommMonoid G] [LinearOrder G] [CommMonoid M] [PartialOrder M] [MulArchimedean M] (f : G →* M)
(hf : StrictMono f) : MulArchimedean G where
arch x _
h := by
refine (MulArchimedean.arch (f x) (by simpa using hf h)).imp ?_
simp [← map_pow, hf.le_iff_le]
