wbtw_smul_vadd_smul_vadd_of_nonpos_of_le

English

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

Русский

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

LaTeX

$$$(r_1 \le 0) \land (r_2 \le r_1) \Rightarrow Wbtw_R\big(r_1 v + x,\; x,\; r_2 v + x\big)$$$

Lean4

theorem wbtw_smul_vadd_smul_vadd_of_nonpos_of_le (x : P) (v : V) {r₁ r₂ : R} (hr₁ : r₁ ≤ 0) (hr₂ : r₂ ≤ r₁) :
    Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) := by
  convert wbtw_smul_vadd_smul_vadd_of_nonneg_of_le x (-v) (Left.nonneg_neg_iff.2 hr₁) (neg_le_neg_iff.2 hr₂) using 1 <;>
    rw [neg_smul_neg]

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