English
Let α be a type with a binary operation, a zero, and a preorder. Suppose left multiplication by any a preserves and reflects the order in the sense of ≤. Then for all b,c ∈ α, b · a ≤ c · a iff b ≤ c, under the appropriate positivity assumptions.
Русский
Пусть α — множество с бинарной операцией, нулем и порядком. Предположим, что левое умножение на любой a сохраняет и отражает порядок по отношению к ≤. Тогда для любых b,c ∈ α выполняется b · a ≤ c · a тогда и только тогда, когда b ≤ c, при соблюдении условий положительности.
LaTeX
$$$\\\\forall \\alpha\\,[Mul\\;\\alpha]\\\\,[Zero\\;\\alpha]\\\\,[Preorder\\;\\alpha]\\,[MulPosMono\\;\\alpha]\\,[MulPosReflectLE\\;\\alpha],\\\\\\\\forall a,b,c\\in \\alpha,\\\\ 0 < a \\rightarrow (b \\cdot a \\le c \\cdot a \\iff b \\le c).$$$
Lean4
@[simp]
theorem mul_le_mul_iff_left₀ [MulPosMono α] [MulPosReflectLE α] (a0 : 0 < a) : b * a ≤ c * a ↔ b ≤ c :=
@rel_iff_cov α>0 α (fun x y => y * x) (· ≤ ·) _ _ ⟨a, a0⟩ _ _
