OAI/Probability/SpanningForest/PathConcatenation.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem336.PathConcatenation.UnitPath line 9
  2. def OAI.Problem336.PathConcatenation.leftEnd line 14
  3. def OAI.Problem336.PathConcatenation.rightEnd line 15
  4. def OAI.Problem336.PathConcatenation.segment line 17
  5. theorem OAI.Problem336.PathConcatenation.continuous_segment line 19
  6. theorem OAI.Problem336.PathConcatenation.segment_eq_zero_of_le line 23
  7. theorem OAI.Problem336.PathConcatenation.segment_eq_endpoint_of_ge line 28
  8. def OAI.Problem336.PathConcatenation.concat line 34
  9. theorem OAI.Problem336.PathConcatenation.concat_eq_sum line 35
  10. theorem OAI.Problem336.PathConcatenation.continuous_concat line 41
  11. def OAI.Problem336.PathConcatenation.concatPath line 51
  12. theorem OAI.Problem336.PathConcatenation.concat_nonpos line 52
  13. theorem OAI.Problem336.PathConcatenation.continuous_segment_joint line 54
  14. theorem OAI.Problem336.PathConcatenation.continuous_concat_joint line 65
  15. theorem OAI.Problem336.PathConcatenation.continuous_concatPath line 77
  16. theorem OAI.Problem336.PathConcatenation.measurable_concatPath line 80
  17. theorem OAI.Problem336.PathConcatenation.segment_at_nat_add line 82
  18. theorem OAI.Problem336.PathConcatenation.concat_nat_add line 88
  19. theorem OAI.Problem336.PathConcatenation.concat_nat line 102
  20. theorem OAI.Problem336.PathConcatenation.concat_increment_same_segment line 106
  21. theorem OAI.Problem336.PathConcatenation.concat_nat_add_of_start_zero line 112