OAI/Analysis/CircleDomains/Topology/SimpleArcsProof.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Small path approximations give local path connectivity; minimization of interval oscillations erases loops, and a monotone separating coordinate removes the remaining constant pauses.

  1. lemma OAI.CircleDomainRigidity.exists_injective_subpath line 15
  2. theorem OAI.CircleDomainRigidity.hasSimpleArcsInConnectedOpens_compact_metric line 28

    Source documentation

    Lorimer's connected-open simple-arc specialization.

    theorem hasSimpleArcsInConnectedOpens_compact_metric
    (X : Type*) [MetricSpace X] [CompactSpace X] [LocallyConnectedSpace X] :
    HasSimpleArcsInConnectedOpens X := by
…

    Mentions: OAI.CircleDomainRigidity.HasSimpleArcsInConnectedOpens