OAI/Analysis/CircleDomains/Topology/CompactReductionIntersections.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compact simple-arc reduction for the actual endpoint code law, with its pointwise density bound and all closed-set intersection bounds.

  1. theorem OAI.CircleDomainRigidity.exists_compact_arc_reduction_with_selection line 21
  2. theorem OAI.CircleDomainRigidity.exists_compact_arc_reduction_with_intersections line 65