Tau-sign counting lemmas

Combinatorial lemmas connecting the tau-sign product over vertices to the number of outgoing flags, via the incoming/outgoing partition.

Incoming and outgoing flags are equinumerous

theorem RS.card_in_eq_card_out (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) : {f ∈ F.flags | o.isOut f = false}.card = {f ∈ F.flags | o.isOut f = true}.card

The match bijection gives equal cardinalities of incoming and outgoing flags.

The out-count as a Fintype.card

theorem RS.card_out_eq_fintype (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) : {f ∈ F.flags | o.isOut f = true}.card = Fintype.card { f : ↥F.flags // o.isOut ↑f = true }

The outgoing-flag filter cardinality equals the Fintype.card of the corresponding subtype.