OAI/Probability/StrongRayleigh/GroupExhaustion.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336AdditiveD139.groupEnumeration line 13
  2. theorem OAI.Problem336AdditiveD139.groupEnumeration_surjective line 16
  3. def OAI.Problem336AdditiveD139.groupBaseExhaustion line 19
  4. theorem OAI.Problem336AdditiveD139.one_mem_groupBaseExhaustion line 23
  5. theorem OAI.Problem336AdditiveD139.groupBaseExhaustion_monotone line 28
  6. theorem OAI.Problem336AdditiveD139.mem_groupBaseExhaustion_eventually line 33
  7. def OAI.Problem336AdditiveD139.translatedGroupExhaustion line 41
  8. theorem OAI.Problem336AdditiveD139.self_mem_translatedGroupExhaustion line 45
  9. theorem OAI.Problem336AdditiveD139.translatedGroupExhaustion_monotone line 50
  10. theorem OAI.Problem336AdditiveD139.mem_translatedGroupExhaustion_eventually line 56
  11. theorem OAI.Problem336AdditiveD139.subset_translatedGroupExhaustion_eventually line 63
  12. theorem OAI.Problem336AdditiveD139.translatedGroupExhaustion_equivariant line 77
  13. theorem OAI.Problem336AdditiveD139.iUnion_translatedGroupExhaustion line 89
  14. def OAI.Problem336AdditiveD139.groupExhaustionLimsup line 96
  15. theorem OAI.Problem336AdditiveD139.groupExhaustionLimsup_equivariant line 100