wbtw_or_wbtw_smul_vadd_of_nonpos — Mathlib

English

If r1 ≤ 0 and r2 ≤ 0, then either Wbtw_R x (r1·v + x) (r2·v + x) or the swapped order holds.

Русский

Если r1 ≤ 0 и r2 ≤ 0, то либо Wbtw_R x (r1·v + x) (r2·v + x), либо перестановка: Wbtw_R x (r2·v + x) (r1·v + x).

LaTeX

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

Lean4

theorem wbtw_or_wbtw_smul_vadd_of_nonpos (x : P) (v : V) {r₁ r₂ : R} (hr₁ : r₁ ≤ 0) (hr₂ : r₂ ≤ 0) :
    Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) ∨ Wbtw R x (r₂ • v +ᵥ x) (r₁ • v +ᵥ x) :=
  by
  rcases le_total r₁ r₂ with (h | h)
  · exact Or.inr (wbtw_smul_vadd_smul_vadd_of_nonpos_of_le x v hr₂ h)
  · exact Or.inl (wbtw_smul_vadd_smul_vadd_of_nonpos_of_le x v hr₁ h)

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