OAI/Analysis/CircleDomains/Topology/BasePathCodes.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The base-code space from the positive-law construction. The defining relations are the actual path-hit and level incidences, with physical length, finite deletions, optional tags, endpoint conditions and collar gates.

  1. structure OAI.CircleDomainRigidity.PathCodeData line 20
  2. def OAI.CircleDomainRigidity.priorHitMass line 38
  3. def OAI.CircleDomainRigidity.AllowedTaggedPath line 41
  4. def OAI.CircleDomainRigidity.EndpointCode line 52
  5. abbrev OAI.CircleDomainRigidity.BasePathCode line 59
  6. theorem OAI.CircleDomainRigidity.measurableSet_allowedTaggedPath line 65
  7. theorem OAI.CircleDomainRigidity.measurableSet_endpointCode line 83
  8. theorem OAI.CircleDomainRigidity.standardBorel_basePathCode line 99
  9. def OAI.CircleDomainRigidity.baseCodePhysicalPath line 111