OAI/Analysis/CircleDomains/Sobolev/LipschitzNullFibers.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Null planar sets meet almost every fiber of a Lipschitz scalar map in a set of zero one-dimensional Hausdorff measure.

  1. lemma OAI.CircleDomainRigidity.planar_hausdorff_two_zero_of_volume_zero line 13
  2. lemma OAI.CircleDomainRigidity.lipschitz_null_fibers line 25