le_smul_iff_one_le_left — Mathlib

English

Given a1 ≤ a2, b1 ≤ b2, a1 > 0 and b2 > 0, we have a1•b1 = a2•b2 iff a1 = a2 and b1 = b2.

Русский

При a1 ≤ a2, b1 ≤ b2, a1 > 0 и b2 > 0 имеем a1•b1 = a2•b2 тогда и только тогда, когда a1 = a2 и b1 = b2.

LaTeX

$$$$ a_1 \le a_2 \quad \land \quad b_1 \le b_2 \quad \land \quad 0 < a_1 \quad \land \quad 0 < b_2 \Rightarrow a_1\cdot b_1 = a_2\cdot b_2 \iff a_1 = a_2 \land b_1 = b_2 $$$$

Lean4

@[simp]
theorem le_smul_iff_one_le_left [SMulPosMono α β] [SMulPosReflectLE α β] (hb : 0 < b) : b ≤ a • b ↔ 1 ≤ a :=
  Iff.trans (by rw [one_smul]) (smul_le_smul_iff_of_pos_right hb)

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