OAI/Analysis/CircleDomains/Rigidity/LocalMaskNeighborhoods.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Away from the finitely many marked singularities, every dust point has a common neighborhood on which each masked coordinate is absent or has one of its given real branches. The mask boundary lies in the domain.

  1. theorem OAI.CircleDomainRigidity.exists_common_mask_branch_neighborhood line 14
  2. theorem OAI.CircleDomainRigidity.exists_common_mask_branch_neighborhood_of_subset line 43