OAI/Combinatorics/HalvingLines/Compactness.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PlanarHalving.RankLimit.RatPoint line 12
2. def OAI.PlanarHalving.RankLimit.ratPoint line 14
3. def OAI.PlanarHalving.RankLimit.lowerGrid line 16
4. lemma OAI.PlanarHalving.RankLimit.lowerGrid_monotone line 19
5. lemma OAI.PlanarHalving.RankLimit.lowerGrid_measurable line 31
6. lemma OAI.PlanarHalving.RankLimit.grid_le_lowerGrid line 39
7. theorem OAI.PlanarHalving.RankLimit.moving_tendsto_of_grid line 45
8. theorem OAI.PlanarHalving.RankLimit.monotone_grid_subsequence line 83
9. theorem OAI.PlanarHalving.Transversality.critical_projection_null line 106
10. theorem OAI.PlanarHalving.Transversality.independent_gradients_ae line 121