le_of_smul_le_smul_of_neg — Mathlib

English

If a < 0 and b1 ≤ b2, then b2 ≤ b1 follows from a•b1 ≤ a•b2.

Русский

Если a < 0 и b1 ≤ b2, то из a·b1 ≤ a·b2 следует b2 ≤ b1.

LaTeX

$$$a<0,\ b_1 \le b_2 \Rightarrow b_2 \le b_1$$$

Lean4

theorem le_of_smul_le_smul_of_neg [PosSMulReflectLE α β] (h : a • b₁ ≤ a • b₂) (ha : a < 0) : b₂ ≤ b₁ :=
  by
  rw [← neg_neg a, neg_smul, neg_smul (-a), neg_le_neg_iff] at h
  exact le_of_smul_le_smul_of_pos_left h <| neg_pos.2 ha

Похожие утверждения