OAI/CategoryTheory/Thomason/FiniteChains.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Finite Chains.

  1. structure OAI.Thomason.FiniteVertexChain line 16
  2. def OAI.Thomason.FiniteVertexChain.linearOrder line 24
  3. instance OAI.Thomason.FiniteVertexChain.finiteType line 31
  4. abbrev OAI.Thomason.FiniteVertexChain.inclusion line 33
  5. def OAI.Thomason.FiniteVertexChain.inter line 35
  6. def OAI.Thomason.FiniteVertexChain.subInclusion line 40
  7. abbrev OAI.Thomason.FiniteVertexChain.Supports line 45
  8. lemma OAI.Thomason.FiniteVertexChain.supports_inter line 48
  9. instance OAI.Thomason.FiniteVertexChain.tableMap_isIso line 56
  10. def OAI.Thomason.FiniteVertexChain.lift line 60
  11. lemma OAI.Thomason.FiniteVertexChain.lift_comp_tableMap line 64
  12. lemma OAI.Thomason.FiniteVertexChain.lift_natural line 68
  13. lemma OAI.Thomason.FiniteVertexChain.table_subInclusion_restrict line 77
  14. def OAI.Thomason.FiniteVertexChain.liftAt line 87
  15. lemma OAI.Thomason.FiniteVertexChain.liftAt_natural line 90
  16. lemma OAI.Thomason.FiniteVertexChain.liftAt_independent line 98
  17. lemma OAI.Thomason.FiniteVertexChain.liftAt_table line 104
  18. lemma OAI.Thomason.FiniteVertexChain.restrict_truncate line 109
  19. lemma OAI.Thomason.FiniteVertexChain.restrict_composable line 116
  20. lemma OAI.Thomason.FiniteVertexChain.restrict_comp line 125
  21. def OAI.Thomason.tableChainSupport line 144
  22. lemma OAI.Thomason.tableChainSupport_supports line 148
  23. def OAI.Thomason.posetTableInverseMap line 151
  24. lemma OAI.Thomason.posetTableInverseMap_eq line 155
  25. def OAI.Thomason.posetTableInverse line 159
  26. lemma OAI.Thomason.posetTableInverse_comp_tableMap line 193
  27. lemma OAI.Thomason.posetTableInverse_on_chain line 199
  28. def OAI.Thomason.finiteRangeChain line 213
  29. def OAI.Thomason.finiteRangeFactor line 221
  30. lemma OAI.Thomason.posetTableInverse_finite_natural line 228
  31. lemma OAI.Thomason.posetCategorificationTableMap_comp_inverse line 247
  32. instance OAI.Thomason.posetCategorificationTableMap_isIso line 258