OAI/CategoryTheory/Thomason/RankedFaithfulness.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Ranked Faithfulness.

  1. lemma OAI.Thomason.DirectedComplex.RankedAtoms.table_rank_split line 18
  2. lemma OAI.Thomason.DirectedComplex.RankedAtoms.rank_split line 44
  3. lemma OAI.Thomason.DirectedComplex.RankedAtoms.rank_split_unique line 71
  4. lemma OAI.Thomason.DirectedComplex.RankedAtoms.support_add line 113
  5. lemma OAI.Thomason.DirectedComplex.RankedAtoms.layered_row_above line 123
  6. lemma OAI.Thomason.DirectedComplex.RankedAtoms.layered_bounded line 146
  7. lemma OAI.Thomason.DirectedComplex.RankedAtoms.lower_single_ordered line 155
  8. theorem OAI.Thomason.DirectedComplex.RankedAtoms.ordered_exchange line 176
  9. lemma OAI.Thomason.DirectedComplex.RankedAtoms.AtomPath.index_support line 339
  10. lemma OAI.Thomason.DirectedComplex.RankedAtoms.AtomPath.move_low line 349
  11. lemma OAI.Thomason.DirectedComplex.RankedAtoms.AtomPath.move_high line 394
  12. theorem OAI.Thomason.DirectedComplex.RankedAtoms.layered_ordered line 454
  13. lemma OAI.Thomason.OmegaCategory.Whisker.mono line 537
  14. lemma OAI.Thomason.DirectedComplex.RankedAtoms.basis_injective_on_dim line 556
  15. lemma OAI.Thomason.DirectedComplex.RankedAtoms.whisker_atom_layered line 563
  16. lemma OAI.Thomason.DirectedComplex.RankedAtoms.whisker_layered_of_top line 577
  17. theorem OAI.Thomason.DirectedComplex.RankedAtoms.whiskerFaithful line 587
  18. theorem OAI.Thomason.DirectedComplex.RankedAtoms.hasAdjacentExchange line 603
  19. theorem OAI.Thomason.DirectedComplex.RankedAtoms.onCells_injective_step line 625
  20. theorem OAI.Thomason.GrayRecursive.IntervalHom.chainComparison_finiteSimplex_onCells_bijective line 646
  21. theorem OAI.Thomason.GrayRecursive.IntervalHom.standardSimplexComparison_isIso line 665
  22. theorem OAI.Thomason.main line 683

    Distinct definitions of this name: ComparatorChallenges/ThomasonModelStructures.lean:2460 (different declaration text). Qualify references as OAI.Thomason.main@path.