OAI/RepresentationTheory/UniversalSquare/Contraction/CompactDomainsCore.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Compact Domains Core.

  1. abbrev OAI.Saxl.Columns.CompactDomain line 14
  2. def OAI.Saxl.Columns.CompactDomain.describe line 16
  3. lemma OAI.Saxl.Columns.CompactDomain.mem_describe line 20
  4. def OAI.Saxl.Columns.CompactDomain.full line 24
  5. lemma OAI.Saxl.Columns.CompactDomain.describe_full line 26
  6. def OAI.Saxl.Columns.CompactDomain.atValue line 29
  7. lemma OAI.Saxl.Columns.CompactDomain.describe_atValue line 39
  8. def OAI.Saxl.Columns.CompactDomain.vanished line 87
  9. lemma OAI.Saxl.Columns.CompactDomain.describe_vanished line 89
  10. lemma OAI.Saxl.Columns.compact_sum_sign line 99
  11. def OAI.Saxl.Columns.CompactDomain.mass line 152
  12. lemma OAI.Saxl.Columns.CompactDomain.describe_mass line 156
  13. def OAI.Saxl.Columns.CompactDomains line 164
  14. def OAI.Saxl.Columns.CompactDomains.full line 168
  15. def OAI.Saxl.Columns.CompactDomains.describe line 172
  16. def OAI.Saxl.Columns.CompactDomains.atValue line 176
  17. def OAI.Saxl.Columns.CompactDomains.vanished line 180
  18. def OAI.Saxl.Columns.CompactDomains.mass line 184
  19. lemma OAI.Saxl.Columns.CompactDomains.describe_full line 188
  20. lemma OAI.Saxl.Columns.CompactDomains.describe_atValue line 193
  21. lemma OAI.Saxl.Columns.CompactDomains.describe_vanished line 203
  22. lemma OAI.Saxl.Columns.CompactDomains.describe_mass line 211
  23. def OAI.Saxl.Columns.compactEdgeOptions line 219
  24. lemma OAI.Saxl.Columns.compactEdgeOptions_describe line 225
  25. def OAI.Saxl.Columns.compactOrderEdges line 232
  26. lemma OAI.Saxl.Columns.compactOrderEdges_describe line 237
  27. def OAI.Saxl.Columns.solveCompact line 243
  28. lemma OAI.Saxl.Columns.solveCompact_describe line 255
  29. lemma OAI.Saxl.Columns.contractionInteger_compact line 274