Skip to content

Commit

Permalink
explain parity and ^^^
Browse files Browse the repository at this point in the history
  • Loading branch information
JamesGallicchio committed Jun 9, 2024
1 parent 39f9137 commit 0d7cf1d
Showing 1 changed file with 6 additions and 1 deletion.
7 changes: 6 additions & 1 deletion ITP/triple-orientations.tex
Original file line number Diff line number Diff line change
Expand Up @@ -128,13 +128,18 @@
structure σEquiv (S T : Set Point) where
f : Point → Point
bij : Set.BijOn f S T
parity : Bool -- See Section 4 for details on this field
parity : Bool
σ_eq : ∀ (p ∈ S) (q ∈ S) (r ∈ S), σ p q r = parity ^^^ σ (f p) (f q) (f r)

def OrientationProperty (P : Set Point → Prop) :=
∀ {{S T}}, S ≃σ T → P S → P T -- `≃σ` is infix notation for `σEquiv`
\end{lstlisting}

Our notion of \(\sigma\) equivalence allows for all orientations to be flipped.
The \lstinline{^^^} (xor) operation does nothing when \lstinline{parity} is false,
and negates the orientation when \lstinline{parity} is true.
See~\Cref{sec:symmetry-breaking} for more details.

To illustrate how these notions will be used, let us consider the property
\(
\pi_k(S) \triangleq \text{\em ``pointset } S \text{ contains an empty convex } k\text{-gon''}
Expand Down

0 comments on commit 0d7cf1d

Please sign in to comment.