OAI/CategoryTheory/Thomason/PrismBasis.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Prism Basis.

  1. lemma OAI.Thomason.DirectedComplex.CylinderTables.cylinder_truncated line 16
  2. def OAI.Thomason.GrayRecursive.IntervalHom.chainComparisonOneIso line 52
  3. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparisonOneIso_hom line 64
  4. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparisonOne_isIso line 67
  5. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_posetOne_isIso line 70
  6. def OAI.Thomason.NormalizedChains.Prism.Word line 85
  7. def OAI.Thomason.NormalizedChains.Prism.Word.dim line 89
  8. def OAI.Thomason.NormalizedChains.Prism.Word.rank line 90
  9. def OAI.Thomason.NormalizedChains.Prism.Word.atom line 92
  10. lemma OAI.Thomason.NormalizedChains.Prism.Word.atom_dim line 98
  11. lemma OAI.Thomason.NormalizedChains.Prism.Word.atom_top line 104
  12. lemma OAI.Thomason.NormalizedChains.Prism.Word.atom_rank line 112
  13. lemma OAI.Thomason.NormalizedChains.Prism.Word.dim_eq_of_coefficient line 120
  14. lemma OAI.Thomason.NormalizedChains.Prism.Word.atom_top_support line 125
  15. inductive OAI.Thomason.NormalizedChains.Prism.Basis line 134
  16. def OAI.Thomason.NormalizedChains.Prism.Basis.dim line 142
  17. def OAI.Thomason.NormalizedChains.Prism.Basis.endpointOffset line 146
  18. lemma OAI.Thomason.NormalizedChains.Prism.Basis.endpointOffset_bounds line 149
  19. def OAI.Thomason.NormalizedChains.Prism.Basis.rank line 154
  20. def OAI.Thomason.NormalizedChains.Prism.Basis.atom line 158
  21. def OAI.Thomason.NormalizedChains.Prism.Basis.coefficient line 162
  22. lemma OAI.Thomason.NormalizedChains.Prism.Basis.coefficient_nonneg line 175
  23. lemma OAI.Thomason.NormalizedChains.Prism.Basis.coefficient_endpoint line 189
  24. lemma OAI.Thomason.NormalizedChains.Prism.Basis.atom_bounded line 199
  25. def OAI.Thomason.NormalizedChains.Prism.Basis.boundarySide line 207
  26. lemma OAI.Thomason.NormalizedChains.Prism.Basis.endpointOffset_boundarySide line 209
  27. lemma OAI.Thomason.NormalizedChains.Prism.Basis.coefficient_vertical_endpoint line 214
  28. lemma OAI.Thomason.NormalizedChains.Prism.Basis.coefficient_vertical_vertical line 224
  29. lemma OAI.Thomason.NormalizedChains.Prism.Basis.atom_top_coefficient line 231
  30. theorem OAI.Thomason.NormalizedChains.Prism.Basis.atom_rank line 264