OAI/Analysis/CircleDomains/Selection/SelectableRealFamily.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The already selected real barriers become the seed of mixed selection. All their physical functions and band endpoints are kept, while the temporary label set is the entire dust. Compatibility is kept on the original free set.

  1. theorem OAI.CircleDomainRigidity.exists_selectable_real_family line 22