OAI/Analysis/CircleDomains/Topology/RoundPhaseBoundary.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The selected limiting disk is actually omitted, and its entire circle is a boundary of the image of the original domain.

  1. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.RegularPhaseLimit.circle_image line 17
  2. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.RegularPhaseLimit.finite_map_properties line 23
  3. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.RegularPhaseLimit.omitted_disk line 31
  4. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.RegularPhaseLimit.circle_subset_closure line 45
  5. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.RegularPhaseLimit.circle_subset_frontier line 66