inv_smul_le_iff_of_neg — Mathlib

English

Let a be negative. Then comparing b1 and b2 via left multiplication by a inverse is equivalent to comparing b2 and b1 via left multiplication by a: a⁻¹ • b1 ≤ b2 if and only if a • b2 ≤ b1.

Русский

Пусть a < 0. Тогда отношение между b1 и b2 через умножение слева на a⁻¹ эквивалентно сравнению через a: a⁻¹ • b1 ≤ b2 тогда и только тогда, когда a • b2 ≤ b1.

LaTeX

$$$ a<0 \implies (a^{-1}\cdot b_1 \le b_2 \iff a\cdot b_2 \le b_1) $$$

Lean4

theorem inv_smul_le_iff_of_neg (h : a < 0) : a⁻¹ • b₁ ≤ b₂ ↔ a • b₂ ≤ b₁ := by
  rw [← smul_le_smul_iff_of_neg_left h, smul_inv_smul₀ h.ne]

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