OAI/Probability/SpanningForest/EdgeIID.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem336.EdgeIID.Stream line 20
  2. def OAI.Problem336.EdgeIID.streamLaw line 22
  3. def OAI.Problem336.EdgeIID.stream line 28
  4. theorem OAI.Problem336.EdgeIID.measurable_stream line 30
  5. theorem OAI.Problem336.EdgeIID.map_stream line 33
  6. def OAI.Problem336.EdgeIID.expanded line 36
  7. theorem OAI.Problem336.EdgeIID.measurable_expanded line 38
  8. theorem OAI.Problem336.EdgeIID.map_expanded line 43
  9. def OAI.Problem336.EdgeIID.keys line 55
  10. def OAI.Problem336.EdgeIID.pool line 57
  11. theorem OAI.Problem336.EdgeIID.measurable_keys line 59
  12. theorem OAI.Problem336.EdgeIID.measurable_pool line 62
  13. theorem OAI.Problem336.EdgeIID.map_keys_pool line 66
  14. abbrev OAI.Problem336.EdgeIID.GraphEdge line 92
  15. def OAI.Problem336.EdgeIID.raw line 94
  16. theorem OAI.Problem336.EdgeIID.map_keys_raw line 97
  17. theorem OAI.Problem336.EdgeIID.measurable_coordinate_fixed line 110
  18. theorem OAI.Problem336.EdgeIID.measurable_raw line 115
  19. theorem OAI.Problem336.EdgeIID.map_keys line 122
  20. theorem OAI.Problem336.EdgeIID.ae_injective_keys line 129
  21. theorem OAI.Problem336.EdgeIID.map_raw line 134
  22. theorem OAI.Problem336.EdgeIID.map_rule_of_eq_raw line 144
  23. theorem OAI.Problem336.EdgeIID.map_rule_of_vertexIID line 154
  24. theorem OAI.Problem336.EdgeIID.map_sampled_rule_of_vertexIID line 170