OAI/Analysis/CircleDomains/Topology/ConnectedIndexedNeighborhood.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Shrink each indexed plateau to its connected open component. It still contains the whole disk and meets the original domain.

  1. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRoundDisks.connected_neighborhood line 18
  2. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.connected_indexed_union line 51