OAI/Combinatorics/Chromatic/Witness/WitnessTransport.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.FiniteMatching.align line 12
  2. theorem OAI.ElementaryPositivity.FiniteMatching.align_at line 15
  3. theorem OAI.ElementaryPositivity.FiniteMatching.align_preserves line 19
  4. def OAI.ElementaryPositivity.FiniteMatching.compress line 33
  5. theorem OAI.ElementaryPositivity.FiniteMatching.compress_preserves line 38
  6. theorem OAI.ElementaryPositivity.FiniteMatching.compress_at line 46
  7. theorem OAI.ElementaryPositivity.FiniteMatching.membership_iff line 58
  8. def OAI.ElementaryPositivity.FiniteMatching.cancel line 73
  9. theorem OAI.ElementaryPositivity.FiniteMatching.swap_preserves line 82
  10. theorem OAI.ElementaryPositivity.FiniteMatching.align_energy line 92
  11. theorem OAI.ElementaryPositivity.FiniteMatching.compress_energy line 101
  12. theorem OAI.ElementaryPositivity.FiniteMatching.cancel_energy line 110
  13. def OAI.ElementaryPositivity.ExactMasks.Exact line 126
  14. def OAI.ElementaryPositivity.ExactMasks.Required line 127
  15. def OAI.ElementaryPositivity.ExactMasks.Strict line 128
  16. def OAI.ElementaryPositivity.ExactMasks.GradedEquiv line 130
  17. def OAI.ElementaryPositivity.ExactMasks.strictFibers line 133
  18. def OAI.ElementaryPositivity.ExactMasks.internalStrict line 144
  19. def OAI.ElementaryPositivity.ExactMasks.exactCompl line 153
  20. def OAI.ElementaryPositivity.ExactMasks.strictEquiv line 160
  21. theorem OAI.ElementaryPositivity.ExactMasks.strictEquiv_energy line 168
  22. def OAI.ElementaryPositivity.ExactMasks.step line 178
  23. def OAI.ElementaryPositivity.ExactMasks.refine line 211