OAI/Analysis/CircleDomains/Topology/CountableClosedLevelCount.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Joint Borel measurability of distinct path intersections with a countable union of closed level relations. Paths may retrace themselves.

  1. def OAI.CircleDomainRigidity.indexedSeparatedHits line 20
  2. theorem OAI.CircleDomainRigidity.isClosed_indexedSeparatedHits line 28
  3. theorem OAI.CircleDomainRigidity.measurable_countable_closed_relation_path_count line 58
  4. theorem OAI.CircleDomainRigidity.measurable_sigmaCompact_chart_circle_count line 91
  5. theorem OAI.CircleDomainRigidity.measurable_sigmaCompact_restricted_relation_path_count line 114