wOppSide_smul_vsub_vadd_left — Mathlib

English

If s is an affine subspace and p1,p2 ∈ s, then for x ∈ P and t ≤ 0, s.WOppSide (t·(x − p1) + p2) x.

Русский

Пусть s — аффинное подпространство, p1,p2 ∈ s. Тогда для любого x ∈ P и t ≤ 0, s.WOppSide( t·(x − p1) + p2, x ).

LaTeX

$$$\forall s:\text{AffineSubspace } R P\ ,\forall p_1,p_2\in s\ ,\forall x\in P\ ,\forall t\in R\ , t\le 0\Rightarrow s.WOppSide( t\cdot (x - p_1) + p_2, x).$$$

Lean4

theorem wOppSide_smul_vsub_vadd_left {s : AffineSubspace R P} {p₁ p₂ : P} (x : P) (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) {t : R}
    (ht : t ≤ 0) : s.WOppSide (t • (x -ᵥ p₁) +ᵥ p₂) x :=
  by
  refine ⟨p₂, hp₂, p₁, hp₁, ?_⟩
  rw [vadd_vsub, ← neg_neg t, neg_smul, ← smul_neg, neg_vsub_eq_vsub_rev]
  exact SameRay.sameRay_nonneg_smul_left _ (neg_nonneg.2 ht)

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