OAI/Analysis/CircleDomains/Transfer/PointDustModels.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Source data and a common exterior zero anchor for a finite family of compact tests on a point-complement sphere domain.

  1. def OAI.CircleDomainRigidity.pointDustPathData line 16
  2. theorem OAI.CircleDomainRigidity.point_component_eq_of_totallyDisconnected line 33
  3. theorem OAI.CircleDomainRigidity.plane_complement_nonempty line 41
  4. theorem OAI.CircleDomainRigidity.exists_common_test_anchor line 50