OAI/Computability/DepthThree/HashTriangular.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DepthThreeLowerBound.BinaryHash.exists_last_nonzero line 11
  2. def OAI.DepthThreeLowerBound.BinaryHash.lastIndex line 30
  3. theorem OAI.DepthThreeLowerBound.BinaryHash.lastIndex_nonzero line 33
  4. theorem OAI.DepthThreeLowerBound.BinaryHash.zero_after_lastIndex line 37
  5. theorem OAI.DepthThreeLowerBound.BinaryHash.data_dim_pos line 41
  6. def OAI.DepthThreeLowerBound.BinaryHash.Nonpivot line 44
  7. instance OAI.DepthThreeLowerBound.BinaryHash.(instance at line 47) line 47
  8. theorem OAI.DepthThreeLowerBound.BinaryHash.card_nonpivot line 53
  9. def OAI.DepthThreeLowerBound.BinaryHash.triangularMap line 73
  10. theorem OAI.DepthThreeLowerBound.BinaryHash.triangularMap_injective line 77
  11. theorem OAI.DepthThreeLowerBound.BinaryHash.triangularMap_bijective line 119
  12. def OAI.DepthThreeLowerBound.BinaryHash.triangularEquiv line 131
  13. theorem OAI.DepthThreeLowerBound.BinaryHash.triangularEquiv_fst line 135
  14. theorem OAI.DepthThreeLowerBound.BinaryHash.triangularEquiv_snd line 138