OAI/Analysis/CircleDomains/Selection/RealCoordinateSubfamily.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual real coordinates retained inside a finite masked family.

  1. structure OAI.CircleDomainRigidity.FiniteTransfer.RealCoordinateSubfamily line 12
  2. def OAI.CircleDomainRigidity.FiniteTransfer.RealCoordinateSubfamily.reindex line 28