OAI/CategoryTheory/Thomason/TopSequences.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Top Sequences.

  1. def OAI.Thomason.OmegaCategory.Functor.injectiveImage line 18
  2. def OAI.Thomason.OmegaCategory.Subcategory.preimage line 36
  3. lemma OAI.Thomason.GrayRecursive.IntervalHom.mapCell_injective line 67
  4. lemma OAI.Thomason.GrayRecursive.IntervalHom.ofMap_in_image_iff line 77
  5. def OAI.Thomason.GrayRecursive.IntervalHom.cylinderSubcategory line 92
  6. lemma OAI.Thomason.GrayRecursive.IntervalHom.mem_cylinderSubcategory_iff line 96
  7. lemma OAI.Thomason.GrayRecursive.IntervalHom.endpoint_mem_of_atoms line 106
  8. theorem OAI.Thomason.GrayRecursive.IntervalHom.tensor_mem_of_atoms line 118
  9. theorem OAI.Thomason.GrayRecursive.IntervalHom.tensor_functor_ext_atoms line 172
  10. def OAI.Thomason.NormalizedChains.Prism.Word.coefficient line 208
  11. def OAI.Thomason.NormalizedChains.Prism.Word.rankedAtoms line 214
  12. def OAI.Thomason.NormalizedChains.Prism.Word.ofOrderIso line 234
  13. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_endpoint_basis line 250
  14. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_vertical_basis line 261
  15. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_section_is_inverse line 271
  16. lemma OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_finiteSimplex_isIso_of_section line 297
  17. theorem OAI.Thomason.GrayRecursive.IntervalHom.fullMain_of_standardSimplex_sections line 310
  18. inductive OAI.Thomason.GrayRecursive.IntervalHom.AtomicLayers line 332
  19. lemma OAI.Thomason.GrayRecursive.IntervalHom.AtomicLayers.bounded line 347
  20. def OAI.Thomason.GrayRecursive.IntervalHom.AtomicLayers.subcategory line 363
  21. lemma OAI.Thomason.GrayRecursive.IntervalHom.AtomicLayers.endpoint_cell line 390
  22. lemma OAI.Thomason.GrayRecursive.IntervalHom.AtomicLayers.cylinder_atom line 402
  23. lemma OAI.Thomason.GrayRecursive.IntervalHom.AtomicLayers.vertical_cell line 433
  24. theorem OAI.Thomason.GrayRecursive.IntervalHom.tensor_atomic_layers line 447
  25. inductive OAI.Thomason.OmegaCategory.Whisker line 466
  26. inductive OAI.Thomason.OmegaCategory.TopSequence line 475
  27. lemma OAI.Thomason.OmegaCategory.Whisker.bounded line 484
  28. lemma OAI.Thomason.OmegaCategory.TopSequence.bounded line 497
  29. lemma OAI.Thomason.OmegaCategory.TopSequence.whisker_left line 504
  30. lemma OAI.Thomason.OmegaCategory.TopSequence.whisker_right line 525
  31. lemma OAI.Thomason.OmegaCategory.TopSequence.join line 546
  32. lemma OAI.Thomason.OmegaCategory.TopSequence.comp line 567
  33. def OAI.Thomason.DirectedComplex.RankedAtoms.TopGenerator line 588
  34. lemma OAI.Thomason.DirectedComplex.RankedAtoms.basis_ne_zero line 591
  35. lemma OAI.Thomason.DirectedComplex.RankedAtoms.top_row_join line 597
  36. lemma OAI.Thomason.DirectedComplex.RankedAtoms.top_row_lower line 606
  37. lemma OAI.Thomason.DirectedComplex.RankedAtoms.whisker_top_basis line 612
  38. lemma OAI.Thomason.DirectedComplex.RankedAtoms.fixed_of_top_row_zero line 628
  39. lemma OAI.Thomason.DirectedComplex.RankedAtoms.topSequence_single line 635
  40. lemma OAI.Thomason.DirectedComplex.RankedAtoms.top_and_source_ext line 658
  41. theorem OAI.Thomason.GrayRecursive.IntervalHom.tensor_top_sequence line 695
  42. theorem OAI.Thomason.GrayRecursive.IntervalHom.tensor_single_top_whisker line 734