OAI/Analysis/CircleDomains/Selection/SeededLevelPresentations.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Carry the actual real or mean presentation through the ordered selection, including unused slots filled by the original zero coordinate.

  1. def OAI.CircleDomainRigidity.orderedSelectedPresentations line 17
  2. theorem OAI.CircleDomainRigidity.orderedSelectedPresentations_some line 36
  3. theorem OAI.CircleDomainRigidity.orderedSelectedPresentations_seed line 51
  4. theorem OAI.CircleDomainRigidity.orderedSelectedPresentations_infinite_real line 61