OAI/Analysis/CircleDomains/Topology/CompactArcBoundary.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

On the unit boundary a terminal arc meets only its starting point. Thus atomlessness of the starting law is exactly the needed point avoidance.

  1. theorem OAI.CircleDomainRigidity.diskTerminalArc_boundary_hit_iff line 15
  2. theorem OAI.CircleDomainRigidity.compactArc_boundary_avoidance line 34