OAI/Analysis/CircleDomains/Topology/PathGates.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Countably many closed collar gates give Borel restrictions on path codes.

  1. def OAI.CircleDomainRigidity.separatedGateViolation line 16
  2. theorem OAI.CircleDomainRigidity.isClosed_separatedGateViolation line 19
  3. def OAI.CircleDomainRigidity.GateRule line 40
  4. theorem OAI.CircleDomainRigidity.gateRule_iff line 43
  5. theorem OAI.CircleDomainRigidity.measurableSet_gateRule line 63
  6. def OAI.CircleDomainRigidity.GateRules line 69
  7. theorem OAI.CircleDomainRigidity.measurableSet_gateRules line 72