one_div_lt

Mathlib.Algebra.Order.Field.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

theorem one_div_lt (ha : 0 < a) (hb : 0 < b) : 1 / a < b ↔ 1 / b < a := by simpa using inv_lt_comm₀ ha hb

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

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

Разделы

Аффилиация

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