OAI/Geometry/RCD/Sobolev/CompactSobolevTests.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Continuous compact Sobolev tests and their canonical lift

  1. def OAI.RegularPointCoordinates.compactSobolevTests line 16
  2. def OAI.RegularPointCoordinates.sobolevTestLift line 30
  3. theorem OAI.RegularPointCoordinates.sobolevTestLift_coe line 34
  4. def OAI.RegularPointCoordinates.compactSobolevTestLift line 38
  5. theorem OAI.RegularPointCoordinates.compactSobolevTestLift_coe line 53