OAI/Combinatorics/BalancedRyser/Construction/HypergraphSemantics.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.PartiteHypergraph.toHypergraph_edgeSet_eq_image line 10
  2. theorem OAI.Balanced.PartiteHypergraph.coe_edgeVertices_injective line 22
  3. theorem OAI.Balanced.PartiteHypergraph.toHypergraph_edgeSet_finite line 28
  4. theorem OAI.Balanced.PartiteHypergraph.toHypergraph_edgeSet_ncard line 33
  5. theorem OAI.Balanced.PartiteHypergraph.toHypergraph_edge_ncard line 39
  6. theorem OAI.Balanced.PartiteHypergraph.toHypergraph_edge_inter_part line 44
  7. theorem OAI.Balanced.PartiteHypergraph.toHypergraph_part_ncard line 51
  8. theorem OAI.Balanced.PartiteHypergraph.toHypergraph_unique_part line 55
  9. theorem OAI.Balanced.PartiteHypergraph.toHypergraph_nonisolated_iff line 63
  10. theorem OAI.Balanced.PartiteHypergraph.toHypergraph_intersecting_iff line 79
  11. theorem OAI.Balanced.PartiteHypergraph.toHypergraph_cover_iff line 100
  12. theorem OAI.Balanced.PartiteHypergraph.toHypergraph_hasCoverNumber_iff line 114
  13. theorem OAI.Balanced.PartiteHypergraph.toHypergraph_matching_card_le_one line 137
  14. theorem OAI.Balanced.PartiteHypergraph.toHypergraph_exists_matching_card_one line 148
  15. theorem OAI.Balanced.balancedCounterexample_set_edge_realization line 164