OAI/Analysis/IrrationalRotation/Rotation/RotationSetProjections.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Invariant233.Rotation.setCoefficient line 12
  2. theorem OAI.Invariant233.Rotation.measurable_setCoefficient line 14
  3. theorem OAI.Invariant233.Rotation.norm_setCoefficient_le line 17
  4. abbrev OAI.Invariant233.Rotation.setProjection line 22
  5. theorem OAI.Invariant233.Rotation.setProjection_mem_algebra line 25
  6. theorem OAI.Invariant233.Rotation.norm_setProjection_le line 29
  7. theorem OAI.Invariant233.Rotation.setProjection_coordinates_ae line 33
  8. theorem OAI.Invariant233.Rotation.setProjection_inter line 39
  9. theorem OAI.Invariant233.Rotation.star_setProjection line 50
  10. theorem OAI.Invariant233.Rotation.isStarProjection_setProjection line 59
  11. theorem OAI.Invariant233.Rotation.setProjection_empty line 66
  12. theorem OAI.Invariant233.Rotation.setProjection_mul_eq_zero_of_disjoint line 75
  13. theorem OAI.Invariant233.Rotation.vacuumFunctional_setProjection line 81
  14. theorem OAI.Invariant233.Rotation.setProjection_univ line 88
  15. theorem OAI.Invariant233.Rotation.setProjection_union line 96
  16. theorem OAI.Invariant233.Rotation.setProjection_biUnion line 118
  17. theorem OAI.Invariant233.Rotation.sum_setProjection_eq_one line 142
  18. theorem OAI.Invariant233.Rotation.U_pow_coordinates_ae line 150
  19. theorem OAI.Invariant233.Rotation.U_pow_mul_setProjection line 162
  20. theorem OAI.Invariant233.Rotation.U_pow_setProjection_star line 187
  21. theorem OAI.Invariant233.Rotation.action_neg_preimage_eq_image line 195
  22. theorem OAI.Invariant233.Rotation.U_pow_setProjection_star_image line 205