OAI/Geometry/RCD/Metric/FiniteMeasureCut.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Quantitative separation of a measure on a finite product

  1. theorem OAI.RegularPointCoordinates.finite_pair_measure_sum line 12
  2. theorem OAI.RegularPointCoordinates.finite_measure_cut_ge_quarter line 23