OAI/Analysis/CircleDomains/Topology/CompactArcStarts.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The boundary start law of compact terminal arcs is atomless whenever each fixed point of the boundary is missed by the original law.

  1. def OAI.CircleDomainRigidity.pathStartLaw line 18
  2. lemma OAI.CircleDomainRigidity.pathStartLaw_singleton_le_hit line 21
  3. lemma OAI.CircleDomainRigidity.pathStartLaw_compl_boundary line 27
  4. theorem OAI.CircleDomainRigidity.pathStartLaw_atomless line 39