OAI/Analysis/CircleDomains/Sobolev/ScalarRegularCoarea.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exact coarea on every bounded Borel set of noncritical differentiability points of a continuous planar scalar function.

  1. lemma OAI.CircleDomainRigidity.scalar_regular_weighted_coarea line 13