OAI/RingTheory/BassTrace/GraphCounting.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BassTrace.Sparse.GraphGeometry.ballMass_recurrence line 51
  2. def OAI.BassTrace.Sparse.GraphGeometry.localTops line 115
  3. lemma OAI.BassTrace.Sparse.GraphGeometry.localTops_finite line 119
  4. lemma OAI.BassTrace.Sparse.GraphGeometry.ballMass_lt_top line 144
  5. lemma OAI.BassTrace.Sparse.GraphCounting.extend_tour line 188
  6. lemma OAI.BassTrace.Sparse.GraphCounting.exists_tour_of_card line 208
  7. theorem OAI.BassTrace.Sparse.GraphCounting.exists_covering_tour line 231
  8. lemma OAI.BassTrace.Sparse.GraphCounting.connected_set_tour line 240
  9. abbrev OAI.BassTrace.Sparse.GraphCounting.BasedWalk line 263
  10. lemma OAI.BassTrace.Sparse.GraphCounting.basedWalk_zero_subsingleton line 265
  11. def OAI.BassTrace.Sparse.GraphCounting.basedWalkSucc line 278
  12. def OAI.BassTrace.Sparse.GraphCounting.basedWalkCons line 282
  13. lemma OAI.BassTrace.Sparse.GraphCounting.basedWalkSucc_injective line 286
  14. lemma OAI.BassTrace.Sparse.GraphCounting.basedWalk_finite line 294
  15. lemma OAI.BassTrace.Sparse.GraphCounting.basedWalk_card_le line 303
  16. abbrev OAI.BassTrace.Sparse.GraphCounting.ConnectedSets line 323
  17. def OAI.BassTrace.Sparse.GraphCounting.connectedSetTour line 326
  18. lemma OAI.BassTrace.Sparse.GraphCounting.connectedSetTour_length line 330
  19. lemma OAI.BassTrace.Sparse.GraphCounting.connectedSetTour_support line 334
  20. def OAI.BassTrace.Sparse.GraphCounting.connectedSetEncoding line 338
  21. lemma OAI.BassTrace.Sparse.GraphCounting.connectedSetEncoding_injective line 342
  22. lemma OAI.BassTrace.Sparse.GraphCounting.connectedSets_finite line 351
  23. theorem OAI.BassTrace.Sparse.GraphCounting.connectedSets_card_le line 356
  24. lemma OAI.BassTrace.Sparse.GraphGeometry.neighborhood_card_bound line 372
  25. lemma OAI.BassTrace.Sparse.GraphGeometry.neighborhood_card_le line 403
  26. lemma OAI.BassTrace.Sparse.GraphGeometry.supportNeighborhood_card_le line 409
  27. abbrev OAI.BassTrace.Sparse.GraphCounting.ConnectedThrough line 426
  28. def OAI.BassTrace.Sparse.GraphCounting.throughEncoding line 430
  29. lemma OAI.BassTrace.Sparse.GraphCounting.throughEncoding_injective line 436
  30. lemma OAI.BassTrace.Sparse.GraphCounting.connectedThrough_finite line 442
  31. theorem OAI.BassTrace.Sparse.GraphCounting.connectedThrough_card_le line 448
  32. lemma OAI.BassTrace.Sparse.GraphGeometry.meeting_simplex_contact line 471
  33. abbrev OAI.BassTrace.Sparse.GraphGeometry.MeetingTops line 486
  34. theorem OAI.BassTrace.Sparse.GraphGeometry.meetingTops_card_le line 491
  35. theorem OAI.BassTrace.Sparse.GraphGeometry.meetingTops_card_le_uniform line 514