one_div_lt_one_div

Mathlib.Algebra.Order.Field.Basic

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

← MathLib Explorer

English

Let a,b > 0. Then 1/b ≤ 1/a iff a ≤ b.

Русский

Пусть a,b > 0. Тогда 1/b ≤ 1/a эквивалентно a ≤ b.

LaTeX

$$$\\forall a,b>0:\\; \\frac{1}{b} \\le \\frac{1}{a} \\iff a \\le b$$$

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 (ha : 0 < a) (hb : 0 < b) : 1 / a < 1 / b ↔ b < a :=
  div_lt_div_iff_of_pos_left zero_lt_one ha hb

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

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

Разделы

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

Аффилиация

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