OAI/Analysis/CircleDomains/Sobolev/SmoothCurveMeasurability.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Measurability of the actual differential-weighted curve fibers is inherited from the published Lipschitz pieces and countable additivity.

  1. theorem OAI.CircleDomainRigidity.aemeasurable_smooth_curve_fiber line 14