OAI/Analysis/CircleDomains/Topology/PathImageCount.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Distinct image intersections with a closed set. Finite separated image witnesses make this count Borel without counting repeated visits.

  1. def OAI.CircleDomainRigidity.pathImageCount line 16
  2. def OAI.CircleDomainRigidity.imageHitAtLeast line 19
  3. def OAI.CircleDomainRigidity.separatedImageHits line 22
  4. theorem OAI.CircleDomainRigidity.isClosed_separatedImageHits line 26
  5. theorem OAI.CircleDomainRigidity.imageHitAtLeast_eq_iUnion line 55
  6. theorem OAI.CircleDomainRigidity.pathImageCount_eq_iSup line 73
  7. theorem OAI.CircleDomainRigidity.measurable_pathImageCount line 113