trans_wOppSide — Mathlib

English

Let S be an affine subspace of P and x,y ∈ P with x and y on opposite sides. Then there exists a point p ∈ S with x, p, y collinear in the sense of a betweenness relation.

Русский

Пусть S — аффинное подпространство P и точки x, y лежат на противоположных сторонах. Тогда существует точка p ∈ S такая, что x, p, y коллинеарны в смысле отношения между двумя точками.

LaTeX

$$$\\\\forall s : \\mathrm{AffineSubspace}\\\\ R P, \\forall x,y : P, s.SOppSide x y \\\\Rightarrow ∃ p ∈ s, Sbtw R x p y$$$

Lean4

theorem trans_wOppSide {s : AffineSubspace R P} {x y z : P} (hxy : s.SOppSide x y) (hyz : s.WOppSide y z) :
    s.WSameSide x z :=
  (hyz.symm.trans_sOppSide hxy.symm).symm

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