OAI/SetTheory/PartitionPrinciple/Geometry/RationalOrderBounds.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Fraction line 7
2. def OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Fraction.Lt line 14
3. def OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Fraction.Equiv line 15
4. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Fraction.den_pos line 17
5. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Fraction.cancel_lt line 19
6. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Fraction.equiv_trans line 27
7. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Fraction.lt_trans line 37
8. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Fraction.lt_left line 47
9. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Fraction.lt_right line 59
10. def OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Fraction.setoid line 71
11. def OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Fraction.mediant line 75
12. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Fraction.mediant_between line 78
13. def OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Fraction.above line 89
14. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Fraction.lt_above line 91
15. def OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Fraction.intCode line 97
16. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Fraction.intCode_injective line 101
17. def OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Fraction.code line 104
18. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Fraction.code_injective line 106
19. def OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Rational line 119
20. def OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Rational.mk line 123
21. def OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Rational.lt line 125
22. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Rational.irrefl line 130
23. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Rational.trans line 134
24. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Rational.compare line 138
25. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Rational.between line 149
26. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Rational.unbounded_above line 153
27. def OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Rational.order line 157
28. def OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Rational.representative line 164
29. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Rational.representative_eq line 167
30. def OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Rational.code line 170
31. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Rational.code_injective line 172
32. def OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Fraction.below line 180
33. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Fraction.below_lt line 182
34. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Rational.mk_eq_iff line 192
35. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Rational.mk_lt_iff line 195
36. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Rational.unbounded_below line 197
37. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Rational.representative_equiv line 201