OAI/Analysis/CircleDomains/Topology/CompactLevelCount.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Joint measurability of actual distinct intersections with a closed level relation. Smooth local circle branches only need continuity on the compact chart piece being counted.

  1. theorem OAI.CircleDomainRigidity.measurable_closed_relation_path_count line 19
  2. theorem OAI.CircleDomainRigidity.measurable_compact_chart_circle_count line 34