lt_or_lt_of_div_lt_div

Mathlib.Algebra.Order.Group.Unbundled.Basic

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

English

If a/d < b/c, then either a < b or c < d.

Русский

Если a/d < b/c, то либо a < b, либо c < d.

LaTeX

$$"a/d < b/c \Rightarrow a < b \lor c < d"$$

Lean4

@[to_additive]
theorem lt_or_lt_of_div_lt_div : a / d < b / c → a < b ∨ c < d := by contrapose!; exact fun h ↦ div_le_div'' h.1 h.2

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

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

Разделы

Аффилиация

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