wSameSide_comm — Mathlib

English

For any affine subspace s and points x,y, the relation WS ameSide is symmetric in x and y: s.WSameSide x y if and only if s.WSameSide y x.

Русский

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

LaTeX

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

Lean4

theorem wSameSide_comm {s : AffineSubspace R P} {x y : P} : s.WSameSide x y ↔ s.WSameSide y x :=
  ⟨fun ⟨p₁, hp₁, p₂, hp₂, h⟩ => ⟨p₂, hp₂, p₁, hp₁, h.symm⟩, fun ⟨p₁, hp₁, p₂, hp₂, h⟩ => ⟨p₂, hp₂, p₁, hp₁, h.symm⟩⟩

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