OAI/Analysis/CircleDomains/Transfer/RealTargetEnds.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Full corresponding target ends and their collapse by actual source tests.

  1. structure OAI.CircleDomainRigidity.FiniteTransfer.RealTargetEnd line 15
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.AssignedRealModelLimit.exists_target_end line 28
  3. def OAI.CircleDomainRigidity.FiniteTransfer.RealTargetEnd.plane line 45
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTargetEnd.cap_antitone line 48
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTargetEnd.plane_inside line 53
  6. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTargetEnd.cap_inside_outer line 59
  7. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTargetEnd.infinity_not_mem line 67
  8. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTargetEnd.sphere_image_plane line 74
  9. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTargetEnd.plane_compact line 82
  10. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTargetEnd.plane_connected line 87
  11. def OAI.CircleDomainRigidity.FiniteTransfer.RealTargetEnd.barrier line 96
  12. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTargetEnd.subsingleton_of_small_tests line 115