OAI/Computability/DepthThree/HashBool.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DepthThreeLowerBound.BinaryHash.hashBool_eq_iff line 11
  2. theorem OAI.DepthThreeLowerBound.BinaryHash.hashBool_collision_iff line 19
  3. def OAI.DepthThreeLowerBound.BinaryHash.hashBool_fiberEquiv line 27
  4. theorem OAI.DepthThreeLowerBound.BinaryHash.hashBool_fiber_card line 34
  5. def OAI.DepthThreeLowerBound.BinaryHash.hashBool_collisionEquiv line 47
  6. theorem OAI.DepthThreeLowerBound.BinaryHash.hashBool_collision_card line 54
  7. def OAI.DepthThreeLowerBound.BinaryHash.boolCoordinateCube line 62
  8. theorem OAI.DepthThreeLowerBound.BinaryHash.mem_boolCoordinateCube_iff line 66
  9. theorem OAI.DepthThreeLowerBound.BinaryHash.injOn_hashBool_iff line 77
  10. def OAI.DepthThreeLowerBound.BinaryHash.hashBool_badSeedEquiv line 96
  11. theorem OAI.DepthThreeLowerBound.BinaryHash.hashBool_badSeed_card_le line 105