OAI/Combinatorics/SumProduct/Alignment/AllLevel14.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AllLevelFactorization.Factorization.ResidueCover.pointEvaluation line 32
  2. lemma OAI.AllLevelFactorization.Factorization.ResidueCover.pointEvaluation_continuous line 37
  3. lemma OAI.AllLevelFactorization.Factorization.ResidueCover.pointEvaluation_rational line 40
  4. def OAI.AllLevelFactorization.Factorization.ResidueCover.pivotProjection line 50
  5. lemma OAI.AllLevelFactorization.Factorization.ResidueCover.pivotProjection_continuous line 53
  6. lemma OAI.AllLevelFactorization.Factorization.ResidueCover.pivotProjection_rational line 55
  7. lemma OAI.AllLevelFactorization.Factorization.ResidueCover.pivotImage_mk line 59
  8. lemma OAI.AllLevelFactorization.Factorization.ResidueCover.pivotImage_expQuotient line 67
  9. def OAI.AllLevelFactorization.Factorization.ResidueCover.projectedPhysicalData line 109
  10. lemma OAI.AffineOrbitRestriction.physical_faces_of_projected_cubes line 155
  11. lemma OAI.AffineOrbitRestriction.physical_faces_of_filtered_cover line 176
  12. lemma OAI.CubeFaces.empty_cube line 209
  13. lemma OAI.CubeFaces.empty_maxLevel line 213
  14. def OAI.CubeFaces.emptyEvaluation line 218
  15. lemma OAI.CubeFaces.empty_level_iff line 223
  16. def OAI.CubeFaces.emptyConstant line 239
  17. lemma OAI.CubeFaces.emptyEvaluation_constant line 246
  18. lemma OAI.CubeFaces.emptyEvaluation_levels line 250