trans_sSameSide — Mathlib

English

Let S be an affine subspace of P. For any x, y, z in P, if x and y lie on the same weak side of S and y and z lie on the same (strong) side of S, then x and z lie on the same weak side of S.

Русский

Пусть S — аффинное подпространство P. Для любых точек x, y, z ∈ P, если x и y лежат на одной слабой стороне S, а y и z лежат на одной (строгой) стороне S, то x и z лежат на одной слабой стороне S.

LaTeX

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

Lean4

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

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