OAI/Analysis/CircleDomains/Selection/PresentedRealCoordinates.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The analytic real family for a mixed model needs no artificial natural-number ordering. Its actual band widths and functions are obtained from the selected presentations; finite stages retain the inherited order of the whole mixed family.

  1. def OAI.CircleDomainRigidity.realCoordinatesFromPresentations line 21
  2. theorem OAI.CircleDomainRigidity.exists_mixed_exhaustion_from_presentations line 88