wbtw_smul_vadd_smul_vadd_of_nonneg_of_le

English

Let x ∈ P and v ∈ V. If r1 ≤ r2 and r1 ≥ 0, then the three points x, r1·v + x, r2·v + x are weakly between in that order: Wbtw_R x (r1·v + x) (r2·v + x).

Русский

Пусть x ∈ P и v ∈ V. При r1 ≤ r2 и r1 ≥ 0 тройка x, r1·v + x, r2·v + x образуют слабое между: Wbtw_R x (r1·v + x) (r2·v + x).

LaTeX

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

Lean4

theorem wbtw_smul_vadd_smul_vadd_of_nonneg_of_le (x : P) (v : V) {r₁ r₂ : R} (hr₁ : 0 ≤ r₁) (hr₂ : r₁ ≤ r₂) :
    Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x) :=
  by
  refine ⟨r₁ / r₂, ⟨div_nonneg hr₁ (hr₁.trans hr₂), div_le_one_of_le₀ hr₂ (hr₁.trans hr₂)⟩, ?_⟩
  by_cases h : r₁ = 0; · simp [h]
  simp [lineMap_apply, smul_smul, ((hr₁.lt_of_ne' h).trans_le hr₂).ne.symm]

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