OAI/RepresentationTheory/UniversalSquare/Contraction/DomainContractions.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Domain Contractions.

  1. def OAI.Saxl.Columns.Domains line 15
  2. def OAI.Saxl.Columns.Domains.full line 19
  3. def OAI.Saxl.Columns.Domains.weight line 23
  4. lemma OAI.Saxl.Columns.Domains.full_weight line 27
  5. def OAI.Saxl.Columns.Domains.atValue line 33
  6. lemma OAI.Saxl.Columns.Domains.atValue_weight line 37
  7. def OAI.Saxl.Columns.Domains.vanished line 55
  8. lemma OAI.Saxl.Columns.Domains.weight_eq_zero line 59
  9. def OAI.Saxl.Columns.Domains.mass line 72
  10. lemma OAI.Saxl.Columns.Domains.mass_eq_sum line 76
  11. abbrev OAI.Saxl.Columns.Edge line 88
  12. def OAI.Saxl.Columns.domainContraction line 90
  13. lemma OAI.Saxl.Columns.domainContraction_nil line 98
  14. lemma OAI.Saxl.Columns.domainContraction_zero line 105
  15. lemma OAI.Saxl.Columns.triple_indicator_sum line 117
  16. lemma OAI.Saxl.Columns.domainContraction_cons line 130
  17. lemma OAI.Saxl.Columns.domainContraction_perm line 161