one_div_lt_one_div_of_neg

Mathlib.Algebra.Order.Field.Basic

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

← MathLib Explorer

English

For a,b < 0, 1/a < 1/b iff b < a.

Русский

Для a < 0 и b < 0, 1/a < 1/b эквивалентно b < a.

LaTeX

$$$(ha : a < 0) (hb : b < 0) : (1 / a < 1 / b) \iff (b < a)$$$

Lean4

/-- For the single implications with fewer assumptions, see `one_div_lt_one_div_of_lt` and
  `lt_of_one_div_lt_one_div` -/
theorem one_div_lt_one_div_of_neg (ha : a < 0) (hb : b < 0) : 1 / a < 1 / b ↔ b < a :=
  lt_iff_lt_of_le_iff_le (one_div_le_one_div_of_neg hb ha)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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