OAI/Analysis/CircleDomains/Sobolev/SmoothClosedSliceImage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Including the two endpoints of a slice does not increase its image measure. This gives the derivative bound on a closed component segment.

  1. theorem OAI.CircleDomainRigidity.smooth_closed_slice_image_measure_le line 12