OAI/Combinatorics/RamseyFive/Geometry/TreeShape.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.TreeCodec.inorder_map line 10
2. lemma OAI.SharpRamseyFive.TreeCodec.address_card line 17
3. def OAI.SharpRamseyFive.PivotTree.finiteRank line 32
4. lemma OAI.SharpRamseyFive.PivotTree.finiteRank_surjective line 35
5. def OAI.SharpRamseyFive.PivotTree.finiteRankEquiv line 51
6. lemma OAI.SharpRamseyFive.PivotTree.finiteRankEquiv_apply line 55
7. lemma OAI.SharpRamseyFive.PivotTree.finiteRankEquiv_label line 58