OAI/Combinatorics/HalvingLines/SeparatedWindows.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarHalving.TimeWindows.exists_positive_inside line 11
2. lemma OAI.PlanarHalving.TimeWindows.carrier_subset_of_inside line 43
3. lemma OAI.PlanarHalving.TimeWindows.nullSingleton_map_coe line 54
4. lemma OAI.PlanarHalving.TimeWindows.measure_interior_eq line 64
5. lemma OAI.PlanarHalving.RankLimits.three_directions_of_independent line 77
6. lemma OAI.PlanarHalving.Directions.quadrant_allowed line 134
7. lemma OAI.PlanarHalving.RankLimits.actual_forward_limit line 179
8. lemma OAI.PlanarHalving.RankLimits.actual_unoriented_limit line 258
9. theorem OAI.PlanarHalving.RankLimit.jet_diagonal line 315
10. lemma OAI.PlanarHalving.RankLimits.jet_at_physical line 382