OAI/Analysis/CircleDomains/Topology/CircleIntervalTraversal.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual interval traversal used to compare circle embeddings with interval-loop formulations of the Jordan--Schoenflies theorem.

  1. def OAI.CircleDomainRigidity.standardCircleTraversal line 13
  2. lemma OAI.CircleDomainRigidity.continuous_standardCircleTraversal line 15
  3. lemma OAI.CircleDomainRigidity.standardCircleTraversal_closes line 18
  4. lemma OAI.CircleDomainRigidity.standardCircleTraversal_injOn line 21
  5. lemma OAI.CircleDomainRigidity.standardCircleTraversal_image line 31