OAI/NumberTheory/OrdinaryCorrelations/HighTrace/ConnectedSet.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.Rerooting.ConnectedSet line 18
2. structure OAI.OrdinaryCorrelations.Rerooting.Gate line 21
3. lemma OAI.OrdinaryCorrelations.Rerooting.gate_exists line 28
4. lemma OAI.OrdinaryCorrelations.Rerooting.path_append_of_intersection line 36
5. lemma OAI.OrdinaryCorrelations.Rerooting.paths_eq line 51
6. lemma OAI.OrdinaryCorrelations.Rerooting.Gate.factor line 58
7. lemma OAI.OrdinaryCorrelations.Rerooting.Gate.on_path line 67
8. lemma OAI.OrdinaryCorrelations.Rerooting.Gate.support_subset line 73
9. def OAI.OrdinaryCorrelations.Rerooting.Ancestor line 80
10. lemma OAI.OrdinaryCorrelations.Rerooting.path_support_prefix line 83
11. lemma OAI.OrdinaryCorrelations.Rerooting.ancestor_trans line 90
12. lemma OAI.OrdinaryCorrelations.Rerooting.ancestor_irrefl line 105