OAI/Analysis/CircleDomains/Selection/PresentedRealSeed.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The real seed carries the exact presentations needed by the later mixed selection.

  1. theorem OAI.CircleDomainRigidity.exists_presented_real_seed line 16