OAI/Geometry/RCD/Metric/PointedMeasureValues.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Local value integrals under the actual bounded source laws

  1. theorem OAI.RegularPointCoordinates.pointed_measure_image_support line 16
  2. theorem OAI.RegularPointCoordinates.pointed_local_value_integrals line 33