OAI/Analysis/CircleDomains/Selection/ExactRealSelections.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Enumerate the actual real choices without repetition, preserving their chosen lifts and exact band widths. Infinitely many seed labels provide the required infinite index set.

  1. theorem OAI.CircleDomainRigidity.infinite_real_presentations_of_seed line 18
  2. theorem OAI.CircleDomainRigidity.exists_injective_real_presentations line 31