OAI/Analysis/CircleDomains/Transfer/FiniteHoleCore.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual compact region on which a finite-hole differential form must be retained, including its outer and circular boundary curves.

  1. lemma OAI.CircleDomainRigidity.finite_hole_core_closed line 12
  2. lemma OAI.CircleDomainRigidity.jordan_boundary_mem_finite_hole_core line 16
  3. lemma OAI.CircleDomainRigidity.circle_mem_finite_hole_core line 26