nonneg_and_nonneg_or_nonpos_and_nonpos_of_smul_nonneg

English

The same relation between max and min under nonpositive scalar action.

Русский

Та же связь между максимумом и минимумом при неотрицательном действии скаляра.

LaTeX

$$$a \le 0 \Rightarrow a \cdot \max\{b_{1},b_{2}\} = \min\{a\cdot b_{1}, a\cdot b_{2}\}$$$

Lean4

theorem nonneg_and_nonneg_or_nonpos_and_nonpos_of_smul_nonneg (hab : 0 ≤ a • b) : 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 :=
  by
  simp only [Decidable.or_iff_not_not_and_not, not_and, not_le]
  refine fun ab nab ↦ hab.not_gt ?_
  obtain ha | rfl | ha := lt_trichotomy 0 a
  exacts [smul_neg_of_pos_of_neg ha (ab ha.le), ((ab le_rfl).asymm (nab le_rfl)).elim,
    smul_neg_of_neg_of_pos ha (nab ha.le)]

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