OAI/Combinatorics/BalancedRyser/Probability/FourCycle.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.FourCycle.opposite line 10
  2. def OAI.Balanced.FourCycle.SameBlock line 12
  3. def OAI.Balanced.FourCycle.Consecutive line 14
  4. theorem OAI.Balanced.FourCycle.opposite_ne line 16
  5. theorem OAI.Balanced.FourCycle.opposite_opposite line 19
  6. theorem OAI.Balanced.FourCycle.sameBlock_iff line 22
  7. theorem OAI.Balanced.FourCycle.not_sameBlock_iff_consecutive line 26
  8. theorem OAI.Balanced.FourCycle.sameBlock_or_consecutive line 30
  9. def OAI.Balanced.FourCycle.designated line 36
  10. def OAI.Balanced.FourCycle.evenBlock line 39
  11. def OAI.Balanced.FourCycle.oddBlock line 41
  12. theorem OAI.Balanced.FourCycle.mem_designated line 46
  13. theorem OAI.Balanced.FourCycle.point_mem_designated line 50
  14. theorem OAI.Balanced.FourCycle.card_designated line 53
  15. theorem OAI.Balanced.FourCycle.even_union_odd line 57
  16. theorem OAI.Balanced.FourCycle.even_odd_disjoint line 70
  17. theorem OAI.Balanced.FourCycle.card_evenBlock line 79
  18. theorem OAI.Balanced.FourCycle.card_oddBlock line 83
  19. theorem OAI.Balanced.FourCycle.adjacency_of_separated line 89
  20. theorem OAI.Balanced.FourCycle.opposite_uncovered line 98
  21. theorem OAI.Balanced.FourCycle.exists_uncovered line 103
  22. theorem OAI.Balanced.FourCycle.not_covered line 121
  23. theorem OAI.Balanced.FourCycle.sameBlock_pairs line 133
  24. theorem OAI.Balanced.FourCycle.common_block_or_adjacent line 138
  25. theorem OAI.Balanced.FourCycle.external_neighbors_card_le_one line 160