smul_lt_smul_iff_of_pos_right

Mathlib.Algebra.Order.Module.Defs

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

← MathLib Explorer

English

For hb > 0, a1 • b < a2 • b ↔ a1 < a2.

Русский

Для hb > 0, a1 • b < a2 • b эквивалентно a1 < a2.

LaTeX

$$$hb > 0 \Rightarrow (a_1 \cdot b < a_2 \cdot b \iff a_1 < a_2)$$$

Lean4

@[simp]
theorem smul_lt_smul_iff_of_pos_right [SMulPosStrictMono α β] [SMulPosReflectLT α β] (hb : 0 < b) :
    a₁ • b < a₂ • b ↔ a₁ < a₂ :=
  ⟨fun h ↦ lt_of_smul_lt_smul_right h hb.le, fun ha ↦ smul_lt_smul_of_pos_right ha hb⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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