OAI/Analysis/CircleDomains/Selection/AffineTagRestriction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Actual affine restriction of tagged paths. Reparameterized tags keep their old tuples; empty and constant tag pieces become inactive.

  1. def OAI.CircleDomainRigidity.affineRawTag line 16
  2. theorem OAI.CircleDomainRigidity.affineRawTag_interval line 21
  3. theorem OAI.CircleDomainRigidity.affineRawTag_tuple_excluded_iff line 30
  4. def OAI.CircleDomainRigidity.affineRestrictedPath line 43
  5. def OAI.CircleDomainRigidity.affineRestrictedTag line 46
  6. def OAI.CircleDomainRigidity.affineRestrictedTaggedPath line 50
  7. theorem OAI.CircleDomainRigidity.affineRawTag_level_iff line 54
  8. theorem OAI.CircleDomainRigidity.affineRestrictedTag_rules line 59
  9. theorem OAI.CircleDomainRigidity.tagRules_affineRestricted line 76