OAI/Combinatorics/TriangleRemoval/Process/ActivePairMembership.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpTerminalLeave.active_pair_membership line 18
  2. lemma OAI.SharpTerminalLeave.active_pair_sum line 37
  3. lemma OAI.SharpTerminalLeave.sum_finset_as_univ line 59
  4. theorem OAI.SharpTerminalLeave.active_cavityGenerator line 66
  5. lemma OAI.SharpTerminalLeave.active_messageCandidates_card line 94
  6. theorem OAI.SharpTerminalLeave.goodPrefix_cavity_semigroup line 111