OAI/Analysis/CircleDomains/Rigidity/OrderedMaskedSelection.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A selected mixed family retains the complete seed before the new coordinates. Empty selection steps use the seed zero coordinate. The resulting order has type omega plus omega, not a rearranged natural order.

  1. def OAI.CircleDomainRigidity.orderedSelectedCoordinates line 21
  2. theorem OAI.CircleDomainRigidity.freeComponentFailure_mono_free line 30
  3. theorem OAI.CircleDomainRigidity.orderedSelectedCoordinates_compatibility line 36
  4. def OAI.CircleDomainRigidity.orderedSelectedCoordinates_realSubfamily line 134