OAI/Combinatorics/SharpRamsey/Marking/MultiplicityClass.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.MultiplicityClass.weight line 12
2. def OAI.SharpLogRamsey.MultiplicityClass.domain line 14
3. lemma OAI.SharpLogRamsey.MultiplicityClass.weight_mono line 17
4. lemma OAI.SharpLogRamsey.MultiplicityClass.weight_pos line 20
5. lemma OAI.SharpLogRamsey.MultiplicityClass.domain_card line 23
6. theorem OAI.SharpLogRamsey.MultiplicityClass.exists_class line 32