sSameSide_comm — Mathlib

English

For any affine subspace s and points x,y, the relation SS ameSide is symmetric in x and y: s.SSameSide x y iff s.SSameSide y x.

Русский

Для любого аффинного подпространства s и точек x,y отношение SS ameSide симметрично: s.SSameSide x y ⇔ s.SSameSide y x.

LaTeX

$$$\forall s: \text{AffineSubspace}(R,P)\ \forall x,y: P,\; s.SSameSide\; x\; y \iff s.SSameSide\; y\; x$$$

Lean4

theorem sSameSide_comm {s : AffineSubspace R P} {x y : P} : s.SSameSide x y ↔ s.SSameSide y x := by
  rw [SSameSide, SSameSide, wSameSide_comm, and_comm (b := x ∉ s)]

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