OAI/Analysis/CircleDomains/Transfer/RealMarkedModels.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Assign the actual countable real-model terminals to their original source ends.

  1. def OAI.CircleDomainRigidity.FiniteTransfer.CountableRealCoordinates.sourceMark line 15
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.CountableRealCoordinates.sourceMark_outside line 19
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.CountableRealCoordinates.sourceMark_image line 24
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.CountableRealCoordinates.sourceMark_component line 29
  5. def OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.markIndex line 51
  6. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.eventually_markIndex line 57
  7. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.eventually_sourceMark_captured line 63
  8. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.eventually_marked_cap_subset line 78
  9. structure OAI.CircleDomainRigidity.FiniteTransfer.AssignedRealModelLimit line 91
  10. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.exists_assigned_limit line 132