OAI/Analysis/CircleDomains/Topology/PlaneComponentRelation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The closed matched correspondence in the finite source chart. Every point has a singleton fiber or belongs to one of the actual indexed disks.

  1. def OAI.CircleDomainRigidity.MatchedConformalEnds.planeRelation line 16
  2. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.planeRelation_closed line 18
  3. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.plane_fiber_singleton_or_indexed line 23
  4. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.plane_center_interval_represents line 47