mul_nonneg_of_three — Mathlib

English

Among any three elements of a linear ordered ring, at least two have the same sign when multiplied pairwise.

Русский

У трёх элементов линейно упорядоченного кольца по умножению попарно две пары имеют одинаковый знак.

LaTeX

$$$\text{For any }a,b,c\in R:\ 0\le a b \lor 0\le b c \lor 0\le c a$$$

Lean4

/-- Out of three elements of a `LinearOrderedRing`, two must have the same sign. -/
theorem mul_nonneg_of_three [ExistsAddOfLE R] [MulPosStrictMono R] [PosMulStrictMono R] [AddLeftMono R]
    [AddLeftReflectLE R] (a b c : R) : 0 ≤ a * b ∨ 0 ≤ b * c ∨ 0 ≤ c * a :=
  by
  iterate 3 rw [mul_nonneg_iff]
  have or_a := le_total 0 a
  have or_b := le_total 0 b
  have or_c := le_total 0 c
  aesop

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