OAI/Analysis/CircleDomains/Topology/ComponentRelationSelection.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Actual selections from the matched component correspondence. They agree with the conformal map on the domain, are constant on each omitted component, and are continuous at every singleton target fiber.

  1. def OAI.CircleDomainRigidity.MatchedConformalEnds.targetFiber line 17
  2. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.targetFiber_nonempty line 19
  3. def OAI.CircleDomainRigidity.MatchedConformalEnds.selectedTarget line 29
  4. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.selectedTarget_mem line 32
  5. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.selectedTarget_on_domain line 36
  6. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.componentRelation_source_saturated line 40
  7. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.targetFiber_eq_on_component line 59
  8. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.selectedTarget_eq_on_component line 71
  9. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.selectedTarget_continuousAt line 78
  10. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.selectedScalar_neighborhood line 89