trans_wSameSide — Mathlib

English

Let S be an affine subspace of P. If x and y are strictly on the same side of S and y and z are weakly on the same side of S, then x and z are weakly on the same side of S.

Русский

Пусть S — аффинное подпространство P. Если x и y находятся строго на одной стороне S, а y и z — на той же слабой стороне S, то x и z — на той же слабой стороне S.

LaTeX

$$$\\\\forall s : \\mathrm{AffineSubspace}\\\\ R P, \\\\forall x,y,z : P, \\\\; s.SSameSide x y \\\\land\\\\; s.WSameSide y z \\\\Rightarrow s.WSameSide x z$$$

Lean4

theorem trans_wSameSide {s : AffineSubspace R P} {x y z : P} (hxy : s.SSameSide x y) (hyz : s.WSameSide y z) :
    s.WSameSide x z :=
  (hyz.symm.trans_sSameSide hxy.symm).symm

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