OAI/Analysis/CircleDomains/Selection/ActualOneEndedSplicing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The one-ended construction retains an original prefix. Its common prefix and tail budget and compact limits are derived from the input paths.

  1. theorem OAI.CircleDomainRigidity.exists_actual_oneEnded_collar_splicing line 20