OAI/Combinatorics/IndependentSets/Geometry/Witness.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.LargeIndependentSets.(instance at line 8) line 8
2. instance OAI.LargeIndependentSets.mixedTupleDecidableEq line 12
3. abbrev OAI.LargeIndependentSets.LayerImposed.Witness line 18
4. abbrev OAI.LargeIndependentSets.LayerImposed.Arrow line 21
5. def OAI.LargeIndependentSets.LayerImposed.valid line 24
6. instance OAI.LargeIndependentSets.LayerImposed.valid_decidable line 30
7. def OAI.LargeIndependentSets.LayerImposed.arrow line 34
8. def OAI.LargeIndependentSets.LayerImposed.arrowImposed line 38
9. lemma OAI.LargeIndependentSets.LayerImposed.iff_witness line 41
10. instance OAI.LargeIndependentSets.LayerImposed.imposed_decidable line 55