OAI/Analysis/TriangularHilbert/RationalSup.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.TriangularHilbert.RatEndpoints line 11
2. instance OAI.TriangularHilbert.(instance at line 12) line 12
3. def OAI.TriangularHilbert.RatEndpoints.toEndpoints line 14
4. def OAI.TriangularHilbert.cyclicMax line 20
5. lemma OAI.TriangularHilbert.cyclicHard_le_cyclicMax line 23
6. lemma OAI.TriangularHilbert.cyclicMax_eq_iSup line 38
7. def OAI.TriangularHilbert.RatEndpoints.sequence line 48
8. lemma OAI.TriangularHilbert.RatEndpoints.sequence_surjective line 49