inv_smul_lt_iff_of_neg

Mathlib.Algebra.Order.Module.Field

URI: https://scilib.ai/kg/mathlib#inv_smul_lt_iff_of_neg

English

Let a < 0. Then a⁻¹ • b1 < b2 is equivalent to b2 < a • b1.

Русский

Пусть a < 0. Тогда a⁻¹ • b1 < b2 эквивалентно b2 < a • b1.

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru