OAI/Combinatorics/MatchingCount/Machines/TreeSlotIndex.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatchingFPRAS.NumericLadder.coordinateEquiv line 9
2. lemma OAI.MatchingFPRAS.NumericLadder.coordinate_le line 11
3. def OAI.MatchingFPRAS.NumericLadder.coordinateOrderIso line 33
4. lemma OAI.MatchingFPRAS.NumericLadder.slot_card line 35
5. def OAI.MatchingFPRAS.NumericLadder.numberOrderIso line 36
6. lemma OAI.MatchingFPRAS.NumericLadder.slot_index line 45
7. lemma OAI.MatchingFPRAS.NumericLadder.slot_default_zero line 50
8. lemma OAI.MatchingFPRAS.NumericLadder.slot_index_div line 54