English
If for every b > 0 the implication a1•b < a2•b implies a1 < a2 holds, then PosSMulReflectLT α β holds: smul on the left preserves LT reflection for positive b.
Русский
Если для каждого b > 0 выполняется: a1•b < a2•b ⇒ a1 < a2, тогда выполняется PosSMulReflectLT α β: левая операция smul сохраняет отражение LT при положительном b.
LaTeX
$$$$ (\forall b>0\, \forall a_1,a_2:\alpha,\ a_1\cdot b < a_2\cdot b \Rightarrow a_1 < a_2) \Rightarrow PosSMulReflectLT\,\alpha\beta $$$$
Lean4
/-- A constructor for `PosSMulReflectLT` requiring you to prove `a • b₁ < a • b₂ → b₁ < b₂` only
when `0 < a` -/
theorem of_pos (h₀ : ∀ a : α, 0 < a → ∀ b₁ b₂ : β, a • b₁ < a • b₂ → b₁ < b₂) : PosSMulReflectLT α β where
lt_of_smul_lt_smul_left a ha b₁ b₂
h := by
obtain ha | ha := ha.eq_or_lt
· simp [← ha] at h
· exact h₀ _ ha _ _ h
