le_one_div_of_neg

Mathlib.Algebra.Order.Field.Basic

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

English

If a < 0 and b < 0, then a ≤ 1/b iff b ≤ 1/a.

Русский

Если a < 0 и b < 0, то a ≤ 1/b эквивалентно b ≤ 1/a.

LaTeX

$$(a < 0) ∧ (b < 0) ⇒ a ≤ 1/b ⇔ b ≤ 1/a$$

Lean4

theorem le_one_div_of_neg (ha : a < 0) (hb : b < 0) : a ≤ 1 / b ↔ b ≤ 1 / a := by simpa using le_inv_of_neg ha hb

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

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

Разделы

Аффилиация

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