sOppSide_iff_exists_left — Mathlib

English

From Wbtw x y z, there exists a point on the segment determined by x and z which lies on the opposite side w.r.t. y; hence s.OppSide x z holds for some p1,p2.

Русский

Из Wbtw x y z следует, что точка на отрезке xz лежит на противоположной стороне по отношению к y; значит WOppSide x z.

LaTeX

$$$\forall s:\text{AffineSubspace } R P\ ,\forall x,y,z\in P\ (h:Wbtw\ R x y z)\Rightarrow s.WOppSide x z.$$$

Lean4

theorem sOppSide_iff_exists_left {s : AffineSubspace R P} {x y p₁ : P} (h : p₁ ∈ s) :
    s.SOppSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y) :=
  by
  rw [SOppSide, and_comm, wOppSide_iff_exists_left h, and_assoc, and_congr_right_iff]
  intro hx
  rw [or_iff_right hx]

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