OAI/Analysis/CircleDomains/Topology/MapDiskExclusion.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Fixed-circuit exclusions in the compact-open space of maps and disks. The circuit restriction is continuous, so these are the open sets used by countable selection, not just open sets of boundary traces.

  1. abbrev OAI.CircleDomainRigidity.FiniteSource line 16
  2. abbrev OAI.CircleDomainRigidity.MapDiskData line 17
  3. theorem OAI.CircleDomainRigidity.mapDiskData_secondCountable line 19
  4. def OAI.CircleDomainRigidity.circuitRestriction line 25
  5. theorem OAI.CircleDomainRigidity.continuous_circuitRestriction line 28
  6. def OAI.CircleDomainRigidity.mapDiskExclusion line 32
  7. theorem OAI.CircleDomainRigidity.isOpen_mapDiskExclusion line 36
  8. def OAI.CircleDomainRigidity.sourceCircuit line 41
  9. def OAI.CircleDomainRigidity.finiteSourceMap line 45
  10. theorem OAI.CircleDomainRigidity.circuitRestriction_source line 49