wbtw_smul_vadd_smul_vadd_of_nonneg_of_nonpos

English

If r1 ≥ 0 and r2 ≤ 0, then Wbtw_R (r1·v + x) x (r2·v + x).

Русский

Если r1 ≥ 0 и r2 ≤ 0, то Wbtw_R (r1·v + x) x (r2·v + x).

LaTeX

$$$(r_1 \ge 0) \land (r_2 \le 0) \Rightarrow Wbtw_R (r_1 v + x) x (r_2 v + x)$$

Lean4

theorem wbtw_smul_vadd_smul_vadd_of_nonneg_of_nonpos (x : P) (v : V) {r₁ r₂ : R} (hr₁ : 0 ≤ r₁) (hr₂ : r₂ ≤ 0) :
    Wbtw R (r₁ • v +ᵥ x) x (r₂ • v +ᵥ x) := by
  rw [wbtw_comm]
  exact wbtw_smul_vadd_smul_vadd_of_nonpos_of_nonneg x v hr₂ hr₁

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