mul_eq_mul_iff_eq_and_eq — Mathlib

English

If a ≤ c and b ≤ d, then a·b = c·d holds iff a=c and b=d (under left/right strict monotonicity).

Русский

При условии строгой монотонности слева и справа, а·b = c·d верно тогда и только тогда, когда a=c и b=d.

LaTeX

$$$$ \\forall a,c,b,d \\in \\alpha,\n a \\le c \\land b \\le d \\Rightarrow (a \\cdot b = c \\cdot d) \\iff (a=c \\land b=d) $$$$

Lean4

@[to_additive]
theorem mul_eq_mul_iff_eq_and_eq [MulLeftStrictMono α] [MulRightStrictMono α] {a b c d : α} (hac : a ≤ c)
    (hbd : b ≤ d) : a * b = c * d ↔ a = c ∧ b = d :=
  by
  haveI := mulLeftMono_of_mulLeftStrictMono α
  haveI := mulRightMono_of_mulRightStrictMono α
  rw [le_antisymm_iff, eq_true (mul_le_mul' hac hbd), true_and, mul_le_mul_iff_of_ge hac hbd]

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