English
If 𝕜 is a semiring and M is a LinearOrderedMonoid with an action by 𝕜, and if for every positive c the map a ↦ c • a is StrictMono, then M has an OrderedSMul structure over 𝕜.
Русский
Пусть 𝕜 — полугруппа; M — линейно упорядоченный моноид с действием 𝕜. Если для каждого положительного c отображение a ↦ c • a строго монотонно, то существует упорядоченное действие 𝕜 на M.
LaTeX
$$$ \forall 𝕜 M\,[\text{Semiring } 𝕜], [\text{PartialOrder } 𝕜], [\text{AddCommMonoid } M], [\text{LinearOrder } M], [\text{SMulWithZero } 𝕜 M], (\forall c>0,\ \text{StrictMono}(a \mapsto c \cdot a)) \Rightarrow OrderedSMul 𝕜 M. $$$
Lean4
/-- To prove that a linear ordered monoid is an ordered module, it suffices to verify only the first
axiom of `OrderedSMul`. -/
theorem mk'' [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid M] [LinearOrder M] [SMulWithZero 𝕜 M]
(h : ∀ ⦃c : 𝕜⦄, 0 < c → StrictMono fun a : M => c • a) : OrderedSMul 𝕜 M :=
{ smul_lt_smul_of_pos := fun hab hc => h hc hab
lt_of_smul_lt_smul_of_pos := fun hab hc => (h hc).lt_iff_lt.1 hab }
