trans — Mathlib

English

Let S be an affine subspace of P. If x and y lie on the opposite side of S and y and z lie on the opposite side of S, then x and z lie 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.SOppSide x y \\\\land\\\\; s.SOppSide y z \\\\Rightarrow s.SSameSide x z$$$

Lean4

theorem trans {s : AffineSubspace R P} {x y z : P} (hxy : s.SOppSide x y) (hyz : s.SOppSide y z) : s.SSameSide x z :=
  ⟨hxy.trans_wOppSide hyz.1, hxy.2.1, hyz.2.2⟩

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