OAI/Combinatorics/HadwigerCounterexample/SampledGraphs.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.HadwigerCounterexample.Holes line 15
2. def OAI.HadwigerCounterexample.Holes.unit line 24
3. def OAI.HadwigerCounterexample.Holes.conflict line 25
4. theorem OAI.HadwigerCounterexample.Holes.no_self_conflict line 27
5. def OAI.HadwigerCounterexample.Holes.graph line 29
6. theorem OAI.HadwigerCounterexample.Holes.indepNum_graph_le line 34
7. theorem OAI.HadwigerCounterexample.Holes.matching_pairs line 53

   Source documentation

   Enumerate endpoints of an actual maximum connected matching on positions to obtain pairwise disjoint ordered pairs; their raw unit types do not conflict.

   theorem matching_pairs [Fintype V] (x : V → A) :
       let t := connectedMatchingNumber (graph H x)
   …

   Mentions: OAI.HadwigerCounterexample.Holes.graph