OAI/Probability/SpanningForest/EdgeUniformRule.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336.vertexKeys line 13
  2. def OAI.Problem336.vertexPools line 15
  3. theorem OAI.Problem336.measurable_vertexKeys line 18
  4. theorem OAI.Problem336.measurable_vertexPools line 21
  5. theorem OAI.Problem336.measurable_injective_keyField line 24
  6. theorem OAI.Problem336.vertexKeys_relabel line 35
  7. def OAI.Problem336.edgeUniformRule line 38
  8. theorem OAI.Problem336.edgeUniformRule_of_injective line 44
  9. theorem OAI.Problem336.measurable_edgeUniformRule line 51
  10. theorem OAI.Problem336.measurable_edgeUniformRule_uncurried line 70
  11. theorem OAI.Problem336.edgeUniformRule_equivariant line 76
  12. theorem OAI.Problem336.edgeUniformRule_eq_raw line 86
  13. theorem OAI.Problem336.measurable_edgeUniformRule_fixed line 92
  14. theorem OAI.Problem336.edgeUniformRule_law line 97
  15. theorem OAI.Problem336.sampled_edgeUniformRule_law line 106
  16. theorem OAI.Problem336.exists_equivariant_edge_iid_sampler line 119