div_lt_comm₀

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

URI: https://scilib.ai/kg/mathlib#div_lt_comm₀

English

If b > 0 and c > 0, then a/b < c iff a < b·c.

Русский

Пусть b > 0 и c > 0. Тогда a/b < c эквивалентно a < b·c.

LaTeX

$$$0 < b \land 0 < c \rightarrow a/b < c \iff a < b \cdot c$$$

Lean4

theorem div_lt_comm₀ (hb : 0 < b) (hc : 0 < c) : a / b < c ↔ a / c < b := by rw [div_lt_iff₀ hb, div_lt_iff₀' hc]

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

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

Разделы

Аффилиация

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