OAI/NumberTheory/OrdinaryCorrelations/HighTrace/RootNotDestination.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.root_not_destination line 16
  2. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.vertices_eq_insert_destinations line 21
  3. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.tree_vertices_card line 36
  4. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.sum_children line 44
  5. def OAI.OrdinaryCorrelations.NumericalSubtrees.leafVertices line 53
  6. def OAI.OrdinaryCorrelations.NumericalSubtrees.irregularVertices line 56
  7. def OAI.OrdinaryCorrelations.NumericalSubtrees.returnVertices line 59
  8. def OAI.OrdinaryCorrelations.NumericalSubtrees.unaryReturnVertices line 61
  9. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.leaf_subset_returns line 64
  10. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.leaf_card_le line 87
  11. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.irregular_incidence_mass line 95
  12. def OAI.OrdinaryCorrelations.NumericalSubtrees.incidentEdges line 117
  13. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.incident_card_le line 120
  14. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.return_vertices_card line 135
  15. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.unary_return_incidence_card line 142
  16. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.not_noReturnIncidence line 157
  17. theorem OAI.OrdinaryCorrelations.NumericalSubtrees.bad_edges_le line 170
  18. lemma OAI.OrdinaryCorrelations.NumericalSubtrees.length_good_bad_return line 218