OAI/Analysis/CircleDomains/Sobolev/SmoothOpenImageMeasure.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The image length of a smooth function on an arbitrary open subset of a line is bounded by its actual derivative integral. The domain may have countably many interval components.

  1. theorem OAI.CircleDomainRigidity.smooth_open_image_measure_le line 15