one_div_le

Mathlib.Algebra.Order.Field.Basic

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

English

Let a,b > 0. Then 1/a ≤ b if and only if 1/b ≤ a.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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