The cyclic successor on a finite set

DescriptiveComplexity.cycNext S a is the least element of the finite set S above a, or the least element of S when there is none: the successor along S read as a cycle. What a track gadget needs of it: it maps S to itself injectively (DescriptiveComplexity.cycNext_injOn), and a subset of S closed under it whose complement in S is closed too is empty or all of S (DescriptiveComplexity.eq_empty_or_eq_of_cycNext_closed), so that a cycle through S is used entirely or not at all.

def DescriptiveComplexity.above {α : Type} [LinearOrder α] (S : Finset α) (a : α) : Finset α

The elements of S above a.

Equations

• DescriptiveComplexity.above S a = {x ∈ S | a < x}

noncomputable def DescriptiveComplexity.cycNext {α : Type} [LinearOrder α] (S : Finset α) (a : α) : α

The cyclic successor of a along S: the least element of S above a, or the least element of S when a is the greatest.

Equations

• DescriptiveComplexity.cycNext S a = if h : (DescriptiveComplexity.above S a).Nonempty then (DescriptiveComplexity.above S a).min' h else if h' : S.Nonempty then S.min' h' else a

theorem DescriptiveComplexity.cycNext_mem {α : Type} [LinearOrder α] {S : Finset α} (hS : S.Nonempty) (a : α) : cycNext S a ∈ S

theorem DescriptiveComplexity.cycNext_injOn {α : Type} [LinearOrder α] (S : Finset α) : Set.InjOn (cycNext S) ↑S

The cyclic successor is injective on S.

theorem DescriptiveComplexity.eq_empty_or_eq_of_cycNext_closed {α : Type} [LinearOrder α] {S T : Finset α} (hTS : T ⊆ S) (hT : ∀ a ∈ T, cycNext S a ∈ T) (hT' : ∀ a ∈ S, a ∉ T → cycNext S a ∉ T) : T = ∅ ∨ T = S

A subset of S closed under the cyclic successor, whose complement in S is closed too, is empty or all of S.