OAI/Probability/SpanningForest/AllPairObservation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336.AllPairObservation.vertexPairs line 11
  2. theorem OAI.Problem336.AllPairObservation.mem_vertexPairs line 14
  3. theorem OAI.Problem336.AllPairObservation.vertexPairs_mono line 18
  4. def OAI.Problem336.AllPairObservation.observations line 24
  5. theorem OAI.Problem336.AllPairObservation.mem_observations line 29
  6. theorem OAI.Problem336.AllPairObservation.observations_mono line 36
  7. theorem OAI.Problem336.AllPairObservation.self_mem_observations line 43
  8. theorem OAI.Problem336.AllPairObservation.exists_mem_observations line 47
  9. theorem OAI.Problem336.AllPairObservation.eventually_mem_observations line 56
  10. theorem OAI.Problem336.AllPairObservation.measurable_finset_from_membership line 62
  11. theorem OAI.Problem336.AllPairObservation.measurable_observations line 78
  12. theorem OAI.Problem336.AllPairObservation.locallyFinite_relabel line 87
  13. theorem OAI.Problem336.AllPairObservation.locallyFinite_relabel_iff line 94
  14. theorem OAI.Problem336.AllPairObservation.endpoints_mapEdge line 102
  15. theorem OAI.Problem336.AllPairObservation.mem_observations_relabel line 108