English
Let α, β be ordered structures with appropriate positivity and strict monotonicity of scalar multiplication. If a1 ≤ a2 and b1 ≤ b2 with a2>0 and b1>0, then a1·b1 = a2·b2 if and only if a1 = a2 and b1 = b2.
Русский
Пусть α, β упорядочены и во взаимной системе умножения на скаляры соблюдается строгость. При a1 ≤ a2, b1 ≤ b2, a2>0, b1>0: a1·b1 = a2·b2 тогда и только если a1=a2 и b1=b2.
LaTeX
$$$Iff\, (a_1 \cdot b_1 = a_2 \cdot b_2) \;\iff\; (a_1 = a_2) \land (b_1 = b_2)$$$
Lean4
theorem smul_eq_smul_iff_eq_and_eq_of_pos' [PosSMulStrictMono α β] [SMulPosStrictMono α β] (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂)
(h₂ : 0 < a₂) (h₁ : 0 < b₁) : a₁ • b₁ = a₂ • b₂ ↔ a₁ = a₂ ∧ b₁ = b₂ :=
by
refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
simp only [eq_iff_le_not_lt, ha, hb, true_and]
refine ⟨fun ha ↦ h.not_lt ?_, fun hb ↦ h.not_lt ?_⟩
· exact (smul_lt_smul_of_pos_right ha h₁).trans_le (smul_le_smul_of_nonneg_left hb h₂.le)
· exact (smul_le_smul_of_nonneg_right ha h₁.le).trans_lt (smul_lt_smul_of_pos_left hb h₂)
