OAI/Analysis/CircleDomains/Transfer/SourceEndProjection.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

An actual projection from the limiting sphere to the source quotient, using the inverse on the domain and the matched end on its complement.

  1. structure OAI.CircleDomainRigidity.FiniteTransfer.AssignedRealModelLimit.SourceEndAt line 19
  2. def OAI.CircleDomainRigidity.FiniteTransfer.AssignedRealModelLimit.chosenSourceEnd line 25
  3. def OAI.CircleDomainRigidity.FiniteTransfer.AssignedRealModelLimit.sourceProjection line 32
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.AssignedRealModelLimit.sourceProjection_on_image line 38
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.AssignedRealModelLimit.sourceProjection_off_image line 44
  6. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTargetEnd.source_in_cap_of_target_interior line 55
  7. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTargetEnd.projection_in_source_cap line 68