wSameSide₃₂ — Mathlib

English

Symmetric version of the previous lemma: Wbtw implies the same-side relation holds in the swapped pair, i.e., s.WSameSide z y.

Русский

Симметричная версия: из Wbtw следует, что s.WSameSide z y.

LaTeX

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

Lean4

theorem _root_.Wbtw.wSameSide₃₂ {s : AffineSubspace R P} {x y z : P} (h : Wbtw R x y z) (hx : x ∈ s) :
    s.WSameSide z y :=
  (h.wSameSide₂₃ hx).symm

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