OAI/Combinatorics/SharpRamsey/Selection/NullFreeLaw.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpLogRamsey.Selection.Law.asPublic line 14
  2. lemma OAI.SharpLogRamsey.Selection.Law.nullFree_sum line 16
  3. def OAI.SharpLogRamsey.Selection.Law.nullFree line 27
  4. lemma OAI.SharpLogRamsey.Selection.Law.nullFree_integral line 32
  5. lemma OAI.SharpLogRamsey.Selection.Law.nullFree_positive line 35
  6. lemma OAI.SharpLogRamsey.Selection.Law.nullFree_public_integral line 38
  7. lemma OAI.SharpLogRamsey.Selection.Law.prod_sum_swap line 41