English
If 0 ≤ r1 and 0 ≤ r2, then either x, r1v+x, r2v+x is weakly between or the swapped triplet is: Wbtw_R x (r1·v + x) (r2·v + x) ∨ Wbtw_R x (r2·v + x) (r1·v + x).
Русский
Если 0 ≤ r1 и 0 ≤ r2, то либо x, r1v + x, r2v + x образуют слабое между, либо переставленная тройка: Wbtw_R x (r1·v + x) (r2·v + x) ∨ Wbtw_R x (r2·v + x) (r1·v + x).
LaTeX
$$$(0 \le r_1) \land (0 \le r_2) \Rightarrow\ Big( Wbtw_R\big(x, r_1 v + x, r_2 v + x\big) \lor Wbtw_R\big(x, r_2 v + x, r_1 v + x\big) \Big)$$$
Lean4
theorem wbtw_or_wbtw_smul_vadd_of_nonneg (x : P) (v : V) {r₁ r₂ : R} (hr₁ : 0 ≤ r₁) (hr₂ : 0 ≤ r₂) :
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.inl (wbtw_smul_vadd_smul_vadd_of_nonneg_of_le x v hr₁ h)
· exact Or.inr (wbtw_smul_vadd_smul_vadd_of_nonneg_of_le x v hr₂ h)
