OAI/Geometry/RCD/Heat/HeatCylinderGluing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Measurable gluing of compatible local heat-potential limits

The gluing uses a single countable exceptional time set. No agreement or temporal continuity at exceptional times is asserted.

  1. theorem OAI.RegularPointCoordinates.glue_heat_cylinder_limits line 17