OAI/Analysis/CircleDomains/Topology/DomainPathAdmissibility.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Every path of finite physical length which stays off the dust is allowed with inactive tags, for every residual measure and tuple exclusion.

  1. theorem OAI.CircleDomainRigidity.residualTimes_empty_of_avoids line 17
  2. theorem OAI.CircleDomainRigidity.residualImage_empty_of_avoids line 23
  3. theorem OAI.CircleDomainRigidity.residualIncidence_empty_of_avoids line 27
  4. theorem OAI.CircleDomainRigidity.residualConstraintFamily_of_avoids line 36
  5. theorem OAI.CircleDomainRigidity.allowedTaggedPath_of_avoids line 49
  6. theorem OAI.CircleDomainRigidity.domainPath_allowed line 60