English
If for any b > 0 the map a ↦ a•b is monotone on α, then there is a SMulPosMono structure on α β.
Русский
Если для каждого b > 0 отображение a ↦ a•b монотонно на α, то существует структура SMulPosMono на α β.
LaTeX
$$$$\big(\forall b>0\, \forall a_1,a_2:\alpha,\ a_1 \le a_2 \Rightarrow a_1\cdot b \le a_2\cdot b\big) \Rightarrow SMulPosMono\,\alpha\beta $$$$
Lean4
/-- A constructor for `SMulPosMono` requiring you to prove `a₁ ≤ a₂ → a₁ • b ≤ a₂ • b` only when
`0 < b` -/
theorem of_pos (h₀ : ∀ b : β, 0 < b → ∀ a₁ a₂ : α, a₁ ≤ a₂ → a₁ • b ≤ a₂ • b) : SMulPosMono α β where
smul_le_smul_of_nonneg_right b hb a₁ a₂
h := by
obtain hb | hb := hb.eq_or_lt
· simp [← hb]
· exact h₀ _ hb _ _ h
