Membership and uniqueness in the edge and oriented enumerations

The edge and oriented pair lists enumerate each participating flag exactly once. The slot helpers identify the two ends of each edge.

Edge enumeration

theorem RS.attachWith_partEdges_nodup (W : ClosedFragment) (F : EdgeSubset W) : ((partEdges W F).attachWith (fun (x : Fin (edgeCount W)) => x ∈ edgeIndexSet W F) ⋯).Nodup

The attached edge list for edgePairList is duplicate-free.

theorem RS.castAdd_flag_ne_natAdd_flag (W : ClosedFragment) (i : Fin (edgeCount W)) : (starFlagEnum W).symm (Fin.castAdd (edgeCount W) i) ≠ (starFlagEnum W).symm (Fin.natAdd (edgeCount W) i)

The two slots of an edge give distinct flags.

theorem RS.edgePairList_nodup (W : ClosedFragment) (F : EdgeSubset W) : (edgePairList W F).Nodup

The edge-interleaved enumeration is duplicate-free.

theorem RS.mem_edgePairList (W : ClosedFragment) (F : EdgeSubset W) (x : ↥F.flags) : x ∈ edgePairList W F

Every participating flag appears in the edge-interleaved list.

Oriented enumeration

theorem RS.orientedPairList_nodup (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) : (orientedPairList W F o).Nodup

The oriented enumeration is duplicate-free.

theorem RS.mem_orientedPairList (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (x : ↥F.flags) : x ∈ orientedPairList W F o

Every participating flag appears in the oriented list.