OAI/Analysis/CircleDomains/Transfer/RealPresentationTransfer.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Retain every selected real presentation in the mixed transfer, including real barriers chosen after the initial seed. Its physical function and actual marked band widths are the same ones used by the selection.

  1. theorem OAI.CircleDomainRigidity.PhysicalRealCoordinate.boundary_width_le_one line 18
  2. theorem OAI.CircleDomainRigidity.RealCoordinatePresentation.width_le line 35
  3. def OAI.CircleDomainRigidity.realSubfamily_of_presentations line 52
  4. theorem OAI.CircleDomainRigidity.exists_real_subfamily_covering_presentations line 73
  5. theorem OAI.CircleDomainRigidity.exists_real_subfamily_of_selected_presentations line 93