OAI/Analysis/CircleDomains/Topology/FiniteTailDiskSeparation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finitely many source disks can be enlarged so that every remaining disk meets at most one enlargement. The radius-square sum supplies the finite set of large remaining disks.

  1. theorem OAI.CircleDomainRigidity.finite_large_square_summable_radii line 15
  2. theorem OAI.CircleDomainRigidity.dist_centers_le_of_closedBall_inter line 26
  3. theorem OAI.CircleDomainRigidity.exists_finite_tail_disk_separation line 31