OAI/Geometry/RCD/Metric/EventualPointedCompatibility.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compatibility of local limits with only eventual approximation data

  1. theorem OAI.RegularPointCoordinates.eventual_pointed_limits_eqOn line 13