sOppSide_smul_vsub_vadd_left — Mathlib

English

If x ∉ s, p1,p2 ∈ s and t < 0, then the point t(x − p1) + p2 lies on the opposite side of s from x.

Русский

Если x не принадлежит s, а p1,p2 принадлежат s и t < 0, то точка t(x − p1) + p2 лежит на противоположной стороне от s по отношению к x.

LaTeX

$$$\forall s \subseteq P,\ x \notin s,\ p_1,p_2 \in s,\ t<0:\ s.SOppSide\bigl(t\,(x - p_1) + p_2, x\bigr).$$$

Lean4

theorem sOppSide_smul_vsub_vadd_left {s : AffineSubspace R P} {x p₁ p₂ : P} (hx : x ∉ s) (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s)
    {t : R} (ht : t < 0) : s.SOppSide (t • (x -ᵥ p₁) +ᵥ p₂) x :=
  by
  refine ⟨wOppSide_smul_vsub_vadd_left x hp₁ hp₂ ht.le, fun h => hx ?_, hx⟩
  rwa [vadd_mem_iff_mem_direction _ hp₂, s.direction.smul_mem_iff ht.ne, vsub_right_mem_direction_iff_mem hp₁] at h

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