OAI/Analysis/CircleDomains/Topology/CollarDustAvoidance.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The collar constructions preserve avoidance of arbitrary dust sets. Auxiliary infinite tolls enforce the condition only at non-omitted times.

  1. theorem OAI.CircleDomainRigidity.exists_twoEnded_splicing_avoiding_dust line 22
  2. theorem OAI.CircleDomainRigidity.exists_oneEnded_splicing_avoiding_dust line 77