OAI/Geometry/RCD/Metric/MetricLimitAbsoluteContinuity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Absolute continuity of the actual metric-law limit on the open ball

  1. theorem OAI.RegularPointCoordinates.probability_restrict_absolutelyContinuous_of_local line 12
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.metric_limit_absolutelyContinuous line 38