OAI/Analysis/CircleDomains/Selection/SelectedExclusionUnion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every neighborhood chosen by the actual ordered selection is excluded by its common mixed limit, with its original component label retained.

  1. theorem OAI.CircleDomainRigidity.selected_limit_avoids_test_union line 17