instIsStrictOrderedModule — Mathlib

English

If M is an Additive Commutative Monoid with a Partial Order, a real module action, and IsStrictOrderedModule over ℝ, then M is a IsStrictOrderedModule over ℝ≥0.

Русский

Пусть M — аддитивная коммутативная моноида с частичным порядком и структурой модуля над ℝ, и M является строго упорядоченным модулем над ℝ. Тогда M является строго упорядоченным модулем над ℝ≥0.

LaTeX

$$$$ \IsStrictOrderedModule(\\mathbb{R}, M) \\Rightarrow \\IsStrictOrderedModule(\\mathbb{R}_{\\ge 0}, M). $$$$

Lean4

instance instIsStrictOrderedModule {M : Type*} [AddCommMonoid M] [PartialOrder M] [Module ℝ M]
    [IsStrictOrderedModule ℝ M] : IsStrictOrderedModule ℝ≥0 M :=
  Nonneg.instIsStrictOrderedModule

Похожие утверждения