OAI/Geometry/RCD/Sobolev/RemoveExceptionalTimes.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Removing countably many times from a uniformly Lipschitz cylinder

The spatial estimates persist under the unique continuous time extension. Only scalar Lipschitz extension and density of the good times are used.

  1. theorem OAI.RegularPointCoordinates.remove_countable_times line 18