OAI/Combinatorics/SumProduct/Alignment/CoveringSubspace01.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ConstructedWordPlan.GlobalWordPlan.pivot_haar_mass line 42
2. def OAI.ConstructedWordPlan.GlobalWordPlan.ChartedMassAssertion line 97
3. theorem OAI.ConstructedWordPlan.GlobalWordPlan.uniform_pivot_haar line 127
4. theorem OAI.CubeFaces.cube_top_support line 168
5. def OAI.CubeFaces.affineUpper line 179
6. theorem OAI.CubeFaces.affine_face_displacement line 184
7. def OAI.CoveringSubspace.imageRestrict line 216
8. lemma OAI.CoveringSubspace.continuous_imageRestrict line 219
9. theorem OAI.CoveringSubspace.path_mem_subspace line 225
10. theorem OAI.CoveringSubspace.isQuotientMap_imageRestrict line 241