OAI/Analysis/CircleDomains/Rigidity/MatchedMaskDomain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The open domain of the actual mask is connected, and its residual complement is removable dust on the original circle-domain boundary.

  1. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRoundDisks.exists_mask_domain line 17