div_pos_iff — Mathlib

English

For a linear-order field α, a,b ∈ α, we have 0 < a/b if and only if (0 < a and 0 < b) or (a < 0 and b < 0).

Русский

Пусть α — упорядоченное поле; тогда 0 < a/b тогда и только тогда, когда (0 < a и 0 < b) или (a < 0 и b < 0).

LaTeX

$$$0 < \dfrac{a}{b} \quad\Longleftrightarrow\quad (0 < a \land 0 < b) \lor (a < 0 \land b < 0)$$$

Lean4

theorem div_pos_iff : 0 < a / b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0 := by
  simp only [division_def, mul_pos_iff, inv_pos, inv_lt_zero]

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