pos_and_pos_or_neg_and_neg_of_mul_pos

English

If a and b are real numbers in a linear ordered ring and a·b > 0, then either a>0 and b>0 or a<0 and b<0.

Русский

Пусть a и b — числа на линейном упорядоченном кольце; если a·b>0, то либо a>0 и b>0, либо a<0 и b<0.

LaTeX

$$$a\,b > 0 \Rightarrow (a>0 \land b>0) \lor (a<0 \land b<0)$$$

Lean4

theorem pos_and_pos_or_neg_and_neg_of_mul_pos [PosMulMono α] [MulPosMono α] (hab : 0 < a * b) :
    0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0 := by
  rcases lt_trichotomy a 0 with (ha | rfl | ha)
  · refine Or.inr ⟨ha, lt_imp_lt_of_le_imp_le (fun hb => ?_) hab⟩
    exact mul_nonpos_of_nonpos_of_nonneg ha.le hb
  · rw [zero_mul] at hab
    exact hab.false.elim
  · refine Or.inl ⟨ha, lt_imp_lt_of_le_imp_le (fun hb => ?_) hab⟩
    exact mul_nonpos_of_nonneg_of_nonpos ha.le hb

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