OAI/Analysis/CircleDomains/Topology/SubarcMeanCircleCompatibility.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Apply mean-circle compatibility to the actual compact subarc law. Both finite counts and free avoidance are inherited from the original endpoint law through its proved measurable selection witness.

  1. theorem OAI.CircleDomainRigidity.subarc_mean_circle_compatibility line 21