OAI/Computability/VertexCover/Reduction/HonestSelectionCompatible.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.VertexCover.LabelCover.PositionPair line 41
2. abbrev OAI.VertexCover.LabelCover.Seeds line 42
3. def OAI.VertexCover.LabelCover.query line 44
4. theorem OAI.VertexCover.LabelCover.query_left_mem line 48
5. theorem OAI.VertexCover.LabelCover.query_right_mem line 53
6. theorem OAI.VertexCover.LabelCover.query_injective line 58
7. theorem OAI.VertexCover.LabelCover.Query.scope_card_le line 65
8. theorem OAI.VertexCover.LabelCover.Query.localLabel_card_le line 80
9. def OAI.VertexCover.LabelCover.localOfSatisfying line 96
10. def OAI.VertexCover.LabelCover.honestSelection line 100
11. theorem OAI.VertexCover.LabelCover.honestSelection_compatible line 104