OAI/Analysis/CircleDomains/Topology/SmallCompactArcReduction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Every sufficiently deep prescribed collar supports the actual compact simple-arc law with arbitrarily small density and punctured hit norms.

  1. theorem OAI.CircleDomainRigidity.eventually_exists_small_compact_arc_law_with_selection line 19
  2. theorem OAI.CircleDomainRigidity.eventually_exists_small_compact_arc_law line 100