OAI/Geometry/RCD/Heat/ScaledHeatCountableRegions.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous compactness on a countable family of heat cylinders

The reference time and center are the same on every cylinder. This makes the limiting functions agree on their common domains outside one common countable exceptional time set.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.scaled_heat_countable_regions line 23