OAI/Analysis/CircleDomains/Selection/AnchorTailAttachment.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Attach the two outer ends of a limiting block. An anchor containing the limiting junction is handled by truncation or a common domain point.

  1. theorem OAI.CircleDomainRigidity.exists_allowed_anchor_tail_attachment line 21