one_div_le_of_neg

Mathlib.Algebra.Order.Field.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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