OAI/Combinatorics/KMedian/Preparation/CoupledGeometry.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedian.Preparation.Physical line 14
2. def OAI.MetricKMedian.Preparation.physicalCount line 16
3. def OAI.MetricKMedian.Preparation.physicalOpen line 21
4. theorem OAI.MetricKMedian.Preparation.physical_cap line 25
5. theorem OAI.MetricKMedian.Preparation.zero_deficit_total line 43
6. theorem OAI.MetricKMedian.Preparation.physical_mass line 56
7. theorem OAI.MetricKMedian.Preparation.bundle_ball_mass line 68