English
If for every a > 0 the map b ↦ a•b is order-preserving on β, then the left action gives a PosSMulMono structure on α β.
Русский
Если для каждого a > 0 отображение b ↦ a•b сохраняет порядок на β, то левая деяние порождает структуру PosSMulMono на α β.
LaTeX
$$$$\big(\forall a>0\, \forall b_1,b_2\in\beta\, (b_1 \le b_2 \Rightarrow a\cdot b_1 \le a\cdot b_2)\big) \Rightarrow PosSMulMono\,\alpha\beta $$$$
Lean4
/-- A constructor for `PosSMulMono` requiring you to prove `b₁ ≤ b₂ → a • b₁ ≤ a • b₂` only when
`0 < a` -/
theorem of_pos (h₀ : ∀ a : α, 0 < a → ∀ b₁ b₂ : β, b₁ ≤ b₂ → a • b₁ ≤ a • b₂) : PosSMulMono α β where
smul_le_smul_of_nonneg_left a ha b₁ b₂
h := by
obtain ha | ha := ha.eq_or_lt
· simp [← ha]
· exact h₀ _ ha _ _ h
