OAI/Computability/VertexCover/PCP/PoweringWitness.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.UniqueGames.Foundations.PCP.PoweringWitness.iterate_mul_constline 16 - def
OAI.UniqueGames.Foundations.PCP.PoweringWitness.endpointWitnessline 29 - def
OAI.UniqueGames.Foundations.PCP.PoweringWitness.vertexWitnessline 35 - theorem
OAI.UniqueGames.Foundations.PCP.PoweringWitness.endpoint_lower_boundline 40 - theorem
OAI.UniqueGames.Foundations.PCP.PoweringWitness.lazy_middle_witness_meanline 75