OAI/Analysis/CircleDomains/Topology/SphereClusterBridge.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite-chart cluster bounds from the assigned sphere ends

The line-payment lemma uses planar cluster points. They are the same finite cluster values controlled by the inverse terminal-boundary argument, so no boundary extension of the finite uniformization is needed.

  1. theorem OAI.CircleDomainRigidity.planar_mapClusterPt_mem_componentClusterValues line 22
  2. theorem OAI.CircleDomainRigidity.TerminalComponentAssignment.planar_cluster_gap_le line 34
  3. theorem OAI.CircleDomainRigidity.TerminalComponentAssignment.real_planar_cluster_gap_le line 56