OAI/Analysis/CircleDomains/Rigidity/MeanIndexNullTrace.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Null free traces for the actual averaged index on a locally connected prior level continuum. Only connected-open arc existence is supplied by the published topological input; the intersection measure and payment inequality are constructed here.

  1. theorem OAI.CircleDomainRigidity.mean_index_null_trace_on_continuum line 21