OAI/Analysis/CircleDomains/Selection/TagCodeSpace.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Standard Borel ambient codes and Borel simultaneous tag rules.

  1. instance OAI.CircleDomainRigidity.(instance at line 16) line 16
  2. instance OAI.CircleDomainRigidity.(instance at line 22) line 22
  3. def OAI.CircleDomainRigidity.TagRules line 26
  4. theorem OAI.CircleDomainRigidity.measurableSet_tagRules line 34
  5. instance OAI.CircleDomainRigidity.(instance at line 49) line 49
  6. theorem OAI.CircleDomainRigidity.standardBorel_tagRuleCodes line 53