OAI/Analysis/CircleDomains/Selection/FiniteGapGeometry.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Each actual gap of sorted disjoint holes lies in the residual interval.

  1. theorem OAI.CircleDomainRigidity.gapsAfterHoles_subset_residual line 9