OAI/Geometry/TranslativeCovering/BlockSets.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BlockSets.clipped line 29
2. def OAI.BlockSets.cost line 31
3. def OAI.BlockSets.common line 34
4. lemma OAI.BlockSets.clipped_pos line 36
5. lemma OAI.BlockSets.cost_ge line 39
6. lemma OAI.BlockSets.common_measurable line 46
7. lemma OAI.BlockSets.common_subset line 51
8. lemma OAI.BlockSets.choose_sets line 56
9. lemma OAI.BlockSets.intensity_cost line 91
10. lemma OAI.BlockSets.sum_cost line 99