OAI/Combinatorics/BalancedRyser/Local/AlignedUnusedLaw.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.Local.AlignedUnused.usedDirections line 16
  2. abbrev OAI.Balanced.Local.AlignedUnused.UsedArray line 19
  3. abbrev OAI.Balanced.Local.AlignedUnused.UnusedArray line 22
  4. def OAI.Balanced.Local.AlignedUnused.split line 25
  5. theorem OAI.Balanced.Local.AlignedUnused.usedDirections_eq_union line 31
  6. theorem OAI.Balanced.Local.AlignedUnused.aligned_agree line 41
  7. def OAI.Balanced.Local.AlignedUnused.usedAligned line 53
  8. theorem OAI.Balanced.Local.AlignedUnused.aligned_iff_usedAligned line 59
  9. theorem OAI.Balanced.Local.AlignedUnused.alignment_supported line 68
  10. def OAI.Balanced.Local.AlignedUnused.alignedLaw line 83
  11. theorem OAI.Balanced.Local.AlignedUnused.usedAligned_nonempty line 89
  12. def OAI.Balanced.Local.AlignedUnused.usedLaw line 95
  13. theorem OAI.Balanced.Local.AlignedUnused.alignedLaw_eq_uniform_pair line 101
  14. theorem OAI.Balanced.Local.AlignedUnused.alignedLaw_eq_bind line 116
  15. theorem OAI.Balanced.Local.AlignedUnused.alignedLaw_unused line 131
  16. theorem OAI.Balanced.Local.AlignedUnused.alignedLaw_eq_canonical line 145
  17. theorem OAI.Balanced.Local.AlignedUnused.conditionedOffsetProbability_eq_alignedLaw line 151