OAI/Combinatorics/Chromatic/Witness/GraphRequiredPackets.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.NaturalUnitIntervalGraph.nonedgeLT line 15
2. lemma OAI.ElementaryPositivity.NaturalUnitIntervalGraph.nonedgeLT_trans line 16
3. def OAI.ElementaryPositivity.NaturalUnitIntervalGraph.wordMask line 25
4. lemma OAI.ElementaryPositivity.NaturalUnitIntervalGraph.wordMask_empty line 26
5. lemma OAI.ElementaryPositivity.NaturalUnitIntervalGraph.required_sorted line 42
6. lemma OAI.ElementaryPositivity.NaturalUnitIntervalGraph.required_proper line 46
7. lemma OAI.ElementaryPositivity.NaturalUnitIntervalGraph.required_of_sorted line 58
8. abbrev OAI.ElementaryPositivity.NaturalUnitIntervalGraph.RequiredWord line 68
9. abbrev OAI.ElementaryPositivity.NaturalUnitIntervalGraph.PacketColor line 69
10. def OAI.ElementaryPositivity.NaturalUnitIntervalGraph.requiredColorEquiv line 72
11. lemma OAI.ElementaryPositivity.NaturalUnitIntervalGraph.packet_energy line 92
12. lemma OAI.ElementaryPositivity.NaturalUnitIntervalGraph.requiredColorEquiv_energy line 110