OAI/Analysis/CircleDomains/Topology/FullIntervalTag.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A simple arc in a permitted finite level union can use one tag on its whole open parameter interval. If its endpoints are in the domain, no dust time remains and every residual constraint is vacuous.

  1. def OAI.CircleDomainRigidity.fullIntervalTag line 16
  2. def OAI.CircleDomainRigidity.fullIntervalTaggedPath line 20
  3. theorem OAI.CircleDomainRigidity.fullIntervalTag_rules line 25
  4. theorem OAI.CircleDomainRigidity.residualTimes_fullIntervalTaggedPath line 55
  5. theorem OAI.CircleDomainRigidity.residualConstraintFamily_of_empty line 69
  6. theorem OAI.CircleDomainRigidity.fullIntervalTaggedPath_allowed line 84