OAI/Geometry/RCD/Coordinates/VanishingDiagonalCost.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A slowly varying level retaining vanishing nonnegative costs

  1. theorem OAI.RegularPointCoordinates.exists_vanishing_diagonal_cost line 12