OAI/Combinatorics/HalvingLines/Noncollapse.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarHalving.RankLimits.diagonal_common_limit line 11
2. lemma OAI.PlanarHalving.Zoom.compact_scaling_eventually line 72
3. lemma OAI.PlanarHalving.Zoom.radial_of_jet_diagonals line 87
4. lemma OAI.PlanarHalving.RankLimits.actual_radial_comparison line 123
5. lemma OAI.PlanarHalving.Spatial.ray_image_leaves_compact line 182
6. lemma OAI.PlanarHalving.Spatial.radial_upper_enclosure line 203
7. lemma OAI.PlanarHalving.Spatial.radial_lower_exterior line 232
8. lemma OAI.PlanarHalving.Spatial.radial_inner_enclosure line 252
9. lemma OAI.PlanarHalving.RankLimits.allowed_disjoint_in_gap line 271
10. lemma OAI.PlanarHalving.RankLimits.pointwise_radial line 288
11. lemma OAI.PlanarHalving.TimeWindows.exists_two_positive_inside line 350
12. def OAI.PlanarHalving.TimeWindows.CommonChoice line 375
13. instance OAI.PlanarHalving.TimeWindows.(instance at line 378) line 378
14. def OAI.PlanarHalving.TimeWindows.CommonChoice.time line 380
15. lemma OAI.PlanarHalving.TimeWindows.CommonChoice.time_mem line 383
16. lemma OAI.PlanarHalving.TimeWindows.CommonChoice.time_strictMono line 391
17. lemma OAI.PlanarHalving.TimeWindows.CommonChoice.positive_gaps line 398
18. lemma OAI.PlanarHalving.TimeWindows.exists_commonChoice line 414
19. lemma OAI.PlanarHalving.Limits.positive_countable_selection line 428