OAI/Analysis/CircleDomains/Topology/FiniteTerminalDisks.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Round disk coordinates for the actual terminal assignment

The finite model's complementary disks are constructed from its circle domain property. Their labels are exactly the physical terminal labels, and their union is the full complement in the finite chart.

  1. theorem OAI.CircleDomainRigidity.TerminalComponentAssignment.exists_disk_coordinates line 22
  2. theorem OAI.CircleDomainRigidity.terminal_disk_subset_bound line 60