OAI/Analysis/CircleDomains/Topology/MeanCircleCompatibility.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Ordered compatibility of the actual mean circle coordinate follows from the generic intersection laws, finite physical prior lengths, and its proved null traces. No compatibility of the new coordinate is assumed.

  1. theorem OAI.CircleDomainRigidity.mean_circle_compatibility_of_generic_levels line 22