OAI/NumberTheory/OrdinaryCorrelations/HighTrace/ConnectedSetPath.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryCorrelations.Rerooting.connectedSet_path line 18
2. lemma OAI.OrdinaryCorrelations.Rerooting.getVert_mem_drop line 27
3. lemma OAI.OrdinaryCorrelations.Rerooting.mem_drop_index line 36
4. lemma OAI.OrdinaryCorrelations.Rerooting.connectedSet_segment line 44
5. def OAI.OrdinaryCorrelations.Rerooting.segmentIndices line 62
6. lemma OAI.OrdinaryCorrelations.Rerooting.mem_segmentIndices line 65
7. def OAI.OrdinaryCorrelations.Rerooting.rightGate line 69
8. lemma OAI.OrdinaryCorrelations.Rerooting.Gate.vertex_unique line 82
9. lemma OAI.OrdinaryCorrelations.Rerooting.segment_interval line 86