OAI/Computability/PerfectCompleteness/Foundations/LegalOutputLemmas.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PerfectCompleteness.LegalOutput.exists_uniform_target line 17
2. theorem OAI.PerfectCompleteness.CanonicalOutput.leftLabel_card_le_output line 80
3. theorem OAI.PerfectCompleteness.CanonicalOutput.rightLabel_card_le_output line 86
4. theorem OAI.PerfectCompleteness.CanonicalOutput.output_card_positive line 106
5. theorem OAI.PerfectCompleteness.CanonicalOutput.game_value_of_satisfying line 112
6. theorem OAI.PerfectCompleteness.CanonicalOutput.exists_uniform_target line 124