OAI/Analysis/CircleDomains/Rigidity/SubordinateMaskedBranches.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A boundary lying in a common local branch neighborhood gives the actual masked collar data. The finite graph condition then chooses one active coordinate on each filling boundary.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_subordinate_masked_branches line 16