OAI/Analysis/CircleDomains/Topology/TwoEndedCollarSplicing.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Assemble the two actual collar tails and a selected actual middle fragment using the common limiting budget.

  1. def OAI.CircleDomainRigidity.HasShortCollarJoining line 21
  2. theorem OAI.CircleDomainRigidity.exists_twoEnded_collar_splicing_of_limits line 29