pos_and_pos_or_neg_and_neg_of_smul_pos

English

If a•b > 0 for elements a ∈ α, b ∈ β, then either both a and b are positive or both are negative.

Русский

Если A•B > 0 для элементов A ∈ α, B ∈ β, то либо оба положительны, либо оба отрицательны.

LaTeX

$$$$ \text{If } 0 < a \cdot b, \text{ then } (0 < a \land 0 < b) \lor (a < 0 \land b < 0) $$$$

Lean4

theorem pos_and_pos_or_neg_and_neg_of_smul_pos [PosSMulMono α β] [SMulPosMono α β] (hab : 0 < a • b) :
    0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0 := by
  obtain ha | rfl | ha := lt_trichotomy a 0
  · refine Or.inr ⟨ha, lt_imp_lt_of_le_imp_le (fun hb ↦ ?_) hab⟩
    exact smul_nonpos_of_nonpos_of_nonneg ha.le hb
  · rw [zero_smul] at hab
    exact hab.false.elim
  · refine Or.inl ⟨ha, lt_imp_lt_of_le_imp_le (fun hb ↦ ?_) hab⟩
    exact smul_nonpos_of_nonneg_of_nonpos ha.le hb

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