OAI/Geometry/RCD/Metric/CountableTimeCompactness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One time-compactness subsequence for a countable exhaustion

Each spatial region can have its own positive time margin and bounds. The subsequence and exceptional time set are common to every region.

  1. theorem OAI.RegularPointCoordinates.countable_almost_monotone_compactness line 18