OAI/Analysis/CircleDomains/Sobolev/SardProof.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The planar scalar Sard theorem follows from finite-dimensional scalar Sard. Only the dimension-two specialization is used here.

  1. theorem OAI.CircleDomainRigidity.smoothPlanarSard line 13

    Source documentation

    Smooth planar scalar functions have null critical-value sets.

    theorem smoothPlanarSard : SmoothPlanarSard := by
…

    Mentions: OAI.CircleDomainRigidity.SmoothPlanarSard