OAI/NumberTheory/OrdinaryCorrelations/HighTrace/PathTop.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.OrdinaryCorrelations.NumericalSubtrees.pathTopline 19 - def
OAI.OrdinaryCorrelations.NumericalSubtrees.pathRankline 21 - def
OAI.OrdinaryCorrelations.NumericalSubtrees.topMarksline 23 - lemma
OAI.OrdinaryCorrelations.NumericalSubtrees.grows_intersect_topMarksline 26 - theorem
OAI.OrdinaryCorrelations.NumericalSubtrees.chronological_path_hittingline 54