OAI/Analysis/CircleDomains/Topology/SimpleArcPhysicalLocalization.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A simple arc has no occupation atom at its starting point. Thus a terminal arc whose other points lie inside a collar is paid for by the original occupation restricted to that collar.

  1. theorem OAI.CircleDomainRigidity.simple_arc_physical_occupation line 18
  2. theorem OAI.CircleDomainRigidity.simple_arc_physical_support line 25
  3. theorem OAI.CircleDomainRigidity.simple_subarc_physical_localized_le line 42
  4. lemma OAI.CircleDomainRigidity.physicalValue_projects line 55
  5. theorem OAI.CircleDomainRigidity.simple_subarc_physical_collar_le line 63