sOppSide_comm — Mathlib

English

The strong opposite-side relation SOppSide is symmetric in x and y for any affine subspace s: s.SOppSide x y iff s.SOppSide y x.

Русский

Строгое отношение SOppSide симметрично по x и y: s.SOppSide x y ⇔ s.SOppSide y x.

LaTeX

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

Lean4

theorem sOppSide_comm {s : AffineSubspace R P} {x y : P} : s.SOppSide x y ↔ s.SOppSide y x := by
  rw [SOppSide, SOppSide, wOppSide_comm, and_comm (b := x ∉ s)]

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