mul_pos_iff — Mathlib

English

In a linearly ordered ring with requisite monotonicity, 0 < a*b if and only if either a > 0 and b > 0 or a < 0 and b < 0.

Русский

В линейно упорядоченном кольце с необходимыми условиями монотонности 0 < a·b эквивалентно либо a>0 и b>0, либо a<0 и b<0.

LaTeX

$$$0 < a b \iff (0 < a \land 0 < b) \lor (a < 0 \land b < 0)$$$

Lean4

theorem mul_pos_iff [ExistsAddOfLE R] [PosMulStrictMono R] [MulPosStrictMono R] [AddLeftStrictMono R]
    [AddLeftReflectLT R] : 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0 :=
  ⟨pos_and_pos_or_neg_and_neg_of_mul_pos, fun h => h.elim (and_imp.2 mul_pos) (and_imp.2 mul_pos_of_neg_of_neg)⟩

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