OAI/Analysis/CircleDomains/Rigidity/RawArcNullTrace.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual raw barrier has a null free trace on every locally connected compact subcontinuum of a good prior level union. The only arc-existence input is the published connected-open specialization recorded in ArcNullImage.

  1. theorem OAI.CircleDomainRigidity.raw_barrier_null_trace_on_continuum line 16