English
Let α be ordered and β be a β-ordered module over α, with the scalar action preserving nonnegativity in the sense that 0 ≤ a and 0 ≤ b imply 0 ≤ a • b. Then for every a ≥ 0 and b1 ≤ b2 in β, we have a • b1 ≤ a • b2.
Русский
Пусть α упорядочено и β — упорядчённый модуль над α, скалярное действие сохраняет неотрицательность: 0 ≤ a и 0 ≤ b → 0 ≤ a • b. Тогда для каждого a ≥ 0 и b1 ≤ b2 в β выполняется a • b1 ≤ a • b2.
LaTeX
$$$\\forall a \\ge 0, \\; \\forall b_1,b_2 \\in \\beta,\\; b_1 \\le b_2 \\implies a \\cdot b_1 \\le a \\cdot b_2$$$
Lean4
/-- Constructor for `PosSMulMono` when the semimodule is in fact a group. -/
theorem of_smul_nonneg [PartialOrder α] [PartialOrder β] [IsOrderedAddMonoid β]
(h : ∀ a : α, 0 ≤ a → ∀ b : β, 0 ≤ b → 0 ≤ a • b) : PosSMulMono α β where
smul_le_smul_of_nonneg_left _a ha b₁ b₂ := by simpa [sub_nonneg, smul_sub] using h _ ha (b₂ - b₁)
