OAI/Analysis/CircleDomains/Selection/OrderedSelectionSlots.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A selection which adds at most one object per step has an enumeration in its original order. Empty steps are retained as none, so every earlier object occurs at a strictly earlier index.

  1. theorem OAI.CircleDomainRigidity.exists_ordered_selection_slots line 15