OAI/Probability/SpanningForest/WeightedTreeEquiv.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem336.WeightedTree.tree_canonical line 10
  2. def OAI.Problem336.WeightedTree.treeRelabelEquiv line 15
  3. theorem OAI.Problem336.WeightedTree.treeRelabelEquiv_val line 33
  4. def OAI.Problem336.WeightedTree.relabelField line 37
  5. theorem OAI.Problem336.WeightedTree.relabelField_mapEdge line 40
  6. theorem OAI.Problem336.WeightedTree.inclusion_relabel line 45
  7. theorem OAI.Problem336.WeightedTree.finiteField_relabel_mapEdge line 62
  8. theorem OAI.Problem336.WeightedTree.finiteTilt_relabel line 68
  9. theorem OAI.Problem336.WeightedTree.inclusion_congr_on_edges line 87
  10. theorem OAI.Problem336.WeightedTree.extendField_relabel_canonical line 100
  11. theorem OAI.Problem336.WeightedTree.finiteTilt_edgeField_relabel line 109