OAI/Combinatorics/SumProduct/Alignment/CubeFaces02.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CompactGroupProducts.HasCompactReps.map_into line 28
  2. lemma OAI.CompactGroupProducts.HasCompactReps.sup line 41
  3. lemma OAI.CompactGroupProducts.HasCompactReps.compactSpace line 75
  4. lemma OAI.CubeFaces.cube_empty line 96
  5. lemma OAI.CubeFaces.map_upper_cube_le line 108
  6. lemma OAI.CubeFaces.cube_insert_eq line 118
  7. def OAI.CubeFaces.latticeArrays line 124
  8. lemma OAI.CubeFaces.continuous_face line 134
  9. lemma OAI.CubeFaces.continuous_upper line 144
  10. theorem OAI.CubeFaces.cube_hasCompactReps line 155
  11. lemma OAI.CompactGroupProducts.HasCompactReps.comap_subtype line 185
  12. lemma OAI.CompactGroupProducts.HasCompactReps.top_comap_subtype line 201
  13. def OAI.CubeMaxFiltration.clamp line 223
  14. lemma OAI.CubeMaxFiltration.level_eq_clamp_cube line 229
  15. theorem OAI.CubeMaxFiltration.hasCompactReps_level line 236
  16. lemma OAI.CubeLocalHaar.cubeLattice_discrete line 255
  17. theorem OAI.CubeLocalHaar.existsUnique_cubeHaar line 277