pos_iff_pos_of_smul_pos — Mathlib

English

If 0 < a•b, then the signs of a and b agree: 0 < a iff 0 < b (under appropriate monotonicity assumptions on the scalar action).

Русский

Если 0 < a•b, то знаки a и b согласованы: 0 < a тогда и только тогда, когда 0 < b (при соответствующих предпосылках на действие скаляра).

LaTeX

$$$$ 0 < a \cdot b \implies (0 < a \iff 0 < b) $$$$

Lean4

theorem pos_iff_pos_of_smul_pos [PosSMulReflectLT α β] [SMulPosReflectLT α β] (hab : 0 < a • b) : 0 < a ↔ 0 < b :=
  ⟨pos_of_smul_pos_left hab ∘ le_of_lt, pos_of_smul_pos_right hab ∘ le_of_lt⟩

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