OAI/Analysis/CircleDomains/Topology/PathImageSimpleArc.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Loop erasure for a continuous sphere path. Its compact image is a locally connected quotient of the interval, so the published simple-arc input is applied only to the connected open set univ in that image.

  1. theorem OAI.CircleDomainRigidity.locallyConnected_pathTime line 22

    Distinct definitions of this name: OAI/Analysis/CircleDomains/Probability/IntervalPaymentNullImage.lean:16 (different declaration text). Qualify references as OAI.CircleDomainRigidity.locallyConnected_pathTime@path.

  2. theorem OAI.CircleDomainRigidity.exists_simple_subarc line 39