OAI/NumberTheory/OrdinaryCorrelations/HighTrace/VertexIndex.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.NumericalSubtrees.vertexIndex line 18
2. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.vertexIndex_spec line 21
3. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.offset_mem_vertices line 25
4. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.edgeVertices_subset_vertices line 28
5. def OAI.OrdinaryCorrelations.NumericalSubtrees.SameGeometry.vertexImage line 39
6. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.SameGeometry.vertexImage_offset line 41
7. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.SameGeometry.vertexImage_injective line 45
8. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.SameGeometry.vertices_image line 51
9. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.SameGeometry.edgeVertices_image line 54
10. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.SameGeometry.children_image line 58
11. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.SameGeometry.weight line 63
12. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.SameGeometry.modifiedWeight line 73
13. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.SameGeometry.bandDefect line 79
14. def OAI.OrdinaryCorrelations.NumericalSubtrees.SameGeometry.shapeMap line 88
15. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.SameGeometry.shapeMap_edges line 94
16. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.SameGeometry.Shape.ext_edges line 96
17. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.SameGeometry.shapeMap_inverse line 108
18. def OAI.OrdinaryCorrelations.NumericalSubtrees.SameGeometry.shapeEquiv line 111
19. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.SameGeometry.goodEdges line 117