OAI/Probability/FreeIsing/Trees/EdgeLabelCoding.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.EdgeLabelCoding.neighborRank line 16
  2. lemma OAI.Problem367.EdgeLabelCoding.neighborRank_eq_card line 19
  3. lemma OAI.Problem367.EdgeLabelCoding.neighborRank_lt line 22
  4. lemma OAI.Problem367.EdgeLabelCoding.neighborRank_injective line 27
  5. lemma OAI.Problem367.EdgeLabelCoding.neighborRank_lt_degree line 33
  6. lemma OAI.Problem367.EdgeLabelCoding.measurable_neighborRank line 39
  7. def OAI.Problem367.EdgeLabelCoding.edgeIndex line 43
  8. lemma OAI.Problem367.EdgeLabelCoding.adj_symm line 46
  9. lemma OAI.Problem367.EdgeLabelCoding.adj_ne line 48
  10. lemma OAI.Problem367.EdgeLabelCoding.edgeIndex_swap line 54
  11. abbrev OAI.Problem367.EdgeLabelCoding.TreeEdge line 62
  12. lemma OAI.Problem367.EdgeLabelCoding.edgeIndex_injective line 65
  13. lemma OAI.Problem367.EdgeLabelCoding.edgeIndex_snd_lt_degree line 101
  14. lemma OAI.Problem367.EdgeLabelCoding.measurable_edgeIndex line 111
  15. lemma OAI.Problem367.EdgeLabelCoding.measurable_edgeAddresses line 117
  16. lemma OAI.Problem367.EdgeLabelCoding.treeNeighborFinset_image line 124
  17. lemma OAI.Problem367.EdgeLabelCoding.neighborRank_relabel line 137
  18. lemma OAI.Problem367.EdgeLabelCoding.edgeIndex_relabel line 145
  19. def OAI.Problem367.EdgeLabelCoding.edgeLabel line 156
  20. def OAI.Problem367.EdgeLabelCoding.edgeLabels line 159
  21. lemma OAI.Problem367.EdgeLabelCoding.edgeLabel_swap line 162
  22. lemma OAI.Problem367.EdgeLabelCoding.edgeLabel_relabel line 167
  23. lemma OAI.Problem367.EdgeLabelCoding.measurable_edgeLabel line 176
  24. lemma OAI.Problem367.EdgeLabelCoding.measurable_edgeLabels line 183