OAI/Combinatorics/IndependentSets/Reduction/SubchainBase.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.LargeIndependentSets.mixedTupleFintype line 12
2. def OAI.LargeIndependentSets.subchainBase line 18
3. lemma OAI.LargeIndependentSets.subchainBase_le line 21
4. def OAI.LargeIndependentSets.viewFunction line 24
5. theorem OAI.LargeIndependentSets.canonical_subchain_rules line 32