English
If for every b > 0 the implication a1•b < a2•b implies a1 < a2 holds, then PosSMulReflectLT α β holds.
Русский
Если для каждого b>0 выполняется: a1•b < a2•b ⇒ a1 < a2, тогда выполняется PosSMulReflectLT α β.
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 `SMulPosReflectLT` requiring you to prove `a₁ • b < a₂ • b → a₁ < a₂` only
when `0 < b` -/
theorem of_pos (h₀ : ∀ b : β, 0 < b → ∀ a₁ a₂ : α, a₁ • b < a₂ • b → a₁ < a₂) : SMulPosReflectLT α β where
lt_of_smul_lt_smul_right b hb a₁ a₂
h := by
obtain hb | hb := hb.eq_or_lt
· simp [← hb] at h
· exact h₀ _ hb _ _ h
