OAI/Analysis/CircleDomains/Selection/RankedSelectedLevels.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Enumerating the selected labels does not change their inherited order. This supplies exactly the ranked compatibility used by the tag-law proofs.

  1. def OAI.CircleDomainRigidity.selectedCoordinateEnumeration line 19
  2. theorem OAI.CircleDomainRigidity.ranked_compatibility_of_ordered_family line 23
  3. theorem OAI.CircleDomainRigidity.selected_pathData_ranked_compatibility line 44