English
If scalar nonnegativity is preserved and the base ordered additively monoid structure holds, then an IsOrderedModule structure exists on the module.
Русский
Если сохранение неотрицательности при скалярном действии выполнено, и база имеет упорядоченную аддитивную моноиду, то существует структура IsOrderedModule.
LaTeX
$$$\\text{If } \\forall a\\ge 0,\\forall b\\ge 0:\\; a \\cdot b \\ge 0, \\text{ then } IsOrderedModule\\; α\\; β$$$
Lean4
/-- Constructor for `IsOrderedModule` when the semimodule is in fact a module. -/
theorem of_smul_nonneg [IsOrderedAddMonoid α] [IsOrderedAddMonoid β] (h : ∀ a : α, 0 ≤ a → ∀ b : β, 0 ≤ b → 0 ≤ a • b) :
IsOrderedModule α β where
toPosSMulMono := .of_smul_nonneg h
smul_le_smul_of_nonneg_right _b hb a₁ a₂ := by simpa [sub_nonneg, sub_smul] using (h (a₂ - a₁) · _ hb)
