OAI/Geometry/RCD/Sobolev/AlmostMonotoneUniformLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform spatial convergence outside countably many times

The exceptional set is chosen using one countable dense spatial family. Consequently it works simultaneously at every spatial point.

  1. theorem OAI.RegularPointCoordinates.almost_monotone_uniform_limit line 18