wSameSide₂₃ — Mathlib

English

If x,y,z are in the ambient space and h encodes a Wbtw relation, then whenever x ∈ s, y and z lie on the same side of s.

Русский

Если x,y,z образуют отношение Wbtw, и x ∈ s, то y и z лежат на одной стороне s.

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 y z.$$$

Lean4

theorem _root_.Wbtw.wSameSide₂₃ {s : AffineSubspace R P} {x y z : P} (h : Wbtw R x y z) (hx : x ∈ s) :
    s.WSameSide y z := by
  rcases h with ⟨t, ⟨ht0, -⟩, rfl⟩
  exact wSameSide_lineMap_left z hx ht0

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