OAI/Analysis/CircleDomains/Topology/CompactArcIntersections.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The physical compact-arc construction simultaneously retains every closed-set distinct-intersection estimate of the original endpoint law.

  1. theorem OAI.CircleDomainRigidity.exists_compact_physical_arc_law_with_selection line 19
  2. theorem OAI.CircleDomainRigidity.exists_compact_physical_arc_law_with_intersections line 101