OAI/NumberTheory/OrdinaryCorrelations/HighTrace/TreeEdgeInjective.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.OrdinaryCorrelations.NumericalSubtrees.treeEdge_injectiveline 20 - lemma
OAI.OrdinaryCorrelations.NumericalSubtrees.treeEdge_mem_edgeSet_iffline 28 - lemma
OAI.OrdinaryCorrelations.NumericalSubtrees.tour_cutCountline 40 - theorem
OAI.OrdinaryCorrelations.NumericalSubtrees.tree_blocksline 74