OAI/Combinatorics/HalvingLines/ActivityRetention.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarHalving.Boundary.finite_window_params line 11
2. lemma OAI.PlanarHalving.RankLimits.localPartition_subset line 118
3. def OAI.PlanarHalving.RankLimits.subPartition line 121
4. lemma OAI.PlanarHalving.RankLimits.mem_subPartition line 124
5. lemma OAI.PlanarHalving.RankLimits.subPartition_map_val line 134
6. lemma OAI.PlanarHalving.RankLimits.subPartition_sum line 144
7. lemma OAI.PlanarHalving.RankLimits.subPartition_disjoint line 149
8. lemma OAI.PlanarHalving.RankLimits.subPartition_card line 155
9. lemma OAI.PlanarHalving.RankLimits.subPartition_tail line 162
10. lemma OAI.PlanarHalving.Enhancement.limit_vertices_le line 182
11. lemma OAI.PlanarHalving.Enhancement.limit_edge_ac line 188
12. lemma OAI.PlanarHalving.Enhancement.lifted_mass line 213
13. lemma OAI.PlanarHalving.Enhancement.projected_mass line 225
14. lemma OAI.PlanarHalving.Boundary.enhanced_boundary_zero line 237
15. lemma OAI.PlanarHalving.RankLimits.Converges.window_le_edge line 328
16. def OAI.PlanarHalving.RankLimits.commonSet line 335
17. lemma OAI.PlanarHalving.RankLimits.commonSet_measurable line 339
18. lemma OAI.PlanarHalving.RankLimits.Converges.common_positive line 345
19. lemma OAI.PlanarHalving.RankLimits.coordinate_lines_null line 377
20. lemma OAI.PlanarHalving.RankLimits.pairCoordinates_interior_ae line 384