le_one_div

Mathlib.Algebra.Order.Field.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

theorem le_one_div (ha : 0 < a) (hb : 0 < b) : a ≤ 1 / b ↔ b ≤ 1 / a := by simpa using le_inv_comm₀ ha hb

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

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

Разделы

Аффилиация

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