one_div_nonpos — Mathlib

English

Let G be a linearly ordered group with zero, with the property that multiplication by positive elements preserves order. Then the reciprocal 1/a is nonpositive exactly when a is nonpositive; i.e., for all a in G, a^{-1} ≤ 0 if and only if a ≤ 0.

Русский

Пусть G — линейно упорядоченная группа с нулём и умножение на положительные элементы сохраняет порядок. Тогда обратное к элементу неотрицательно тогда и только тогда, когда сам элемент неотрицателен; т.е. для всех a ∈ G выполняется a^{-1} ≤ 0 ⇔ a ≤ 0.

LaTeX

$$$\forall a \in G_0:\; a^{-1} \le 0 \iff a \le 0$$$

Lean4

theorem one_div_nonpos : 1 / a ≤ 0 ↔ a ≤ 0 :=
  one_div a ▸ inv_nonpos

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