OAI/Combinatorics/SumProduct/Alignment/AffineOrbit01.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ConstructedWordPlan.GlobalWordPlan.pivotOptions line 26
  2. lemma OAI.ConstructedWordPlan.GlobalWordPlan.pivotOptions_nonempty line 28
  3. lemma OAI.ConstructedWordPlan.GlobalWordPlan.pivotOptions_paths line 31
  4. def OAI.ConstructedWordPlan.GlobalWordPlan.pivotModulus line 35
  5. lemma OAI.ConstructedWordPlan.GlobalWordPlan.pivotModulus_pos line 38
  6. lemma OAI.ConstructedWordPlan.GlobalWordPlan.pivotOptions_mass line 42
  7. def OAI.ClosedOrbitLift.quotientInclusion line 64
  8. lemma OAI.ClosedOrbitLift.quotientInclusion_mk line 72
  9. lemma OAI.ClosedOrbitLift.quotientInclusion_injective line 76
  10. lemma OAI.ClosedOrbitLift.continuous_quotientInclusion line 89
  11. lemma OAI.ClosedOrbitLift.quotientInclusion_embedding line 95
  12. theorem OAI.ClosedOrbitLift.path_stays_in_subgroup line 103
  13. theorem OAI.ClosedOrbitLift.map_mem_of_projected_orbit line 142
  14. lemma OAI.AffineOrbitRestriction.coset_eq_iff line 176
  15. def OAI.AffineOrbitRestriction.basedHom line 191
  16. lemma OAI.AffineOrbitRestriction.basedHom_apply line 195
  17. lemma OAI.AffineOrbitRestriction.basedHom_continuous line 200
  18. lemma OAI.AffineOrbitRestriction.physical_based line 210
  19. theorem OAI.AffineOrbitRestriction.exists_affine_restriction line 227
  20. def OAI.AffineOrbitRestriction.PreservesPhysicalFaces line 272
  21. lemma OAI.AffineOrbitRestriction.point_preservation_of_faces line 279
  22. lemma OAI.AffineOrbitRestriction.affine_faces_of_physical line 290
  23. theorem OAI.AffineOrbitRestriction.exists_affine_face_restriction line 315