OAI/GroupTheory/FiniteType/SimplexRotation.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SimplexRotation.Std line 24
  2. abbrev OAI.SimplexRotation.Boundary line 25
  3. def OAI.SimplexRotation.minimum line 28
  4. lemma OAI.SimplexRotation.minimum_nonneg line 31
  5. lemma OAI.SimplexRotation.minimum_le line 33
  6. lemma OAI.SimplexRotation.minimum_attained line 35
  7. lemma OAI.SimplexRotation.continuous_minimum line 38
  8. lemma OAI.SimplexRotation.minimum_boundary line 41
  9. def OAI.SimplexRotation.radius line 45
  10. lemma OAI.SimplexRotation.radius_nonneg line 47
  11. lemma OAI.SimplexRotation.radius_zero_iff line 51
  12. lemma OAI.SimplexRotation.continuous_radius line 64
  13. def OAI.SimplexRotation.radial line 67
  14. lemma OAI.SimplexRotation.radial_boundary line 78
  15. def OAI.SimplexRotation.perm line 85
  16. lemma OAI.SimplexRotation.perm_boundary line 94
  17. def OAI.SimplexRotation.mix line 99
  18. lemma OAI.SimplexRotation.mix_zero line 118
  19. lemma OAI.SimplexRotation.mix_one line 120
  20. lemma OAI.SimplexRotation.mix_radius_pos line 123
  21. def OAI.SimplexRotation.boundaryRotation line 147
  22. lemma OAI.SimplexRotation.boundaryRotation_zero line 164
  23. lemma OAI.SimplexRotation.boundaryRotation_one line 172
  24. def OAI.RotationClass.permute line 189
  25. def OAI.RotationClass.blend line 193
  26. lemma OAI.RotationClass.blend_zero line 214
  27. lemma OAI.RotationClass.blend_one line 216
  28. lemma OAI.RotationClass.blend_eq line 218
  29. theorem OAI.RotationClass.class_of_boundary_isotopy line 227
  30. theorem OAI.RotationClass.class_cube line 263
  31. lemma OAI.RotationClass.permute_one line 269
  32. lemma OAI.RotationClass.permute_mul line 279