OAI/Computability/PerfectCompleteness/Reduction/Value.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PerfectCompleteness.Instance.countSatisfied_le_maxSatisfiedline 17 - theorem
OAI.PerfectCompleteness.Instance.maxSatisfied_le_lengthline 22 - theorem
OAI.PerfectCompleteness.Instance.maxSatisfied_attainedline 28 - theorem
OAI.PerfectCompleteness.Instance.value_nonnegline 36 - theorem
OAI.PerfectCompleteness.Instance.value_le_oneline 39 - theorem
OAI.PerfectCompleteness.Instance.rate_le_valueline 44 - theorem
OAI.PerfectCompleteness.Instance.perfectlyComplete_iff_value_eq_oneline 50 - theorem
OAI.PerfectCompleteness.Instance.soundAt_iff_value_leline 68