OAI/Geometry/RCD/Sobolev/BoundedLipschitzProduct.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Product tests needed for restriction of the measured approximation

  1. theorem OAI.RegularPointCoordinates.bounded_unit_lipschitz_product line 13
  2. theorem OAI.RegularPointCoordinates.bounded_lipschitz_product line 32