OAI/Analysis/CircleDomains/Topology/PlaneCriticalFibers.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Bounded plane sets have finite two-dimensional Hausdorff measure; exhaustion therefore removes the finite-measure restriction in the critical-fiber argument.

  1. lemma OAI.CircleDomainRigidity.bounded_plane_hausdorff_two_lt_top line 14
  2. lemma OAI.CircleDomainRigidity.measurableSet_planar_critical line 24
  3. lemma OAI.CircleDomainRigidity.ae_zero_planar_critical_fiber line 36
  4. lemma OAI.CircleDomainRigidity.ae_zero_weighted_planar_critical_fiber line 60