OAI/CategoryTheory/Thomason/RankedAtoms.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Ranked Atoms.

  1. structure OAI.Thomason.DirectedComplex.RankedAtoms line 15
  2. def OAI.Thomason.DirectedComplex.RankedAtoms.basis line 39
  3. lemma OAI.Thomason.DirectedComplex.RankedAtoms.basis_own line 42
  4. lemma OAI.Thomason.DirectedComplex.RankedAtoms.coefficient_basis line 45
  5. lemma OAI.Thomason.DirectedComplex.RankedAtoms.coefficient_eq_zero line 55
  6. lemma OAI.Thomason.DirectedComplex.RankedAtoms.expansion line 60
  7. lemma OAI.Thomason.DirectedComplex.RankedAtoms.basis_positive line 75
  8. lemma OAI.Thomason.DirectedComplex.RankedAtoms.derivative_rank line 82
  9. def OAI.Thomason.DirectedComplex.RankedAtoms.mass line 96
  10. lemma OAI.Thomason.DirectedComplex.RankedAtoms.mass_apply line 98
  11. lemma OAI.Thomason.DirectedComplex.RankedAtoms.mass_nonneg line 101
  12. lemma OAI.Thomason.DirectedComplex.RankedAtoms.mass_basis line 106
  13. lemma OAI.Thomason.DirectedComplex.RankedAtoms.mass_pos line 113
  14. lemma OAI.Thomason.DirectedComplex.RankedAtoms.augmentation_basis line 119
  15. lemma OAI.Thomason.DirectedComplex.RankedAtoms.augmentation_eq_mass line 126
  16. lemma OAI.Thomason.DirectedComplex.RankedAtoms.positive_augmentation_zero line 137
  17. lemma OAI.Thomason.DirectedComplex.RankedAtoms.peel_remainder line 148
  18. lemma OAI.Thomason.DirectedComplex.RankedAtoms.objects_atomic line 161
  19. lemma OAI.Thomason.DirectedComplex.RankedAtoms.peel_positive line 189
  20. inductive OAI.Thomason.DirectedComplex.RankedAtoms.TopPasting line 237
  21. lemma OAI.Thomason.DirectedComplex.RankedAtoms.top_pasting line 244
  22. def OAI.Thomason.DirectedComplex.RankedAtoms.cut line 286
  23. lemma OAI.Thomason.DirectedComplex.RankedAtoms.coefficient_cut line 289
  24. lemma OAI.Thomason.DirectedComplex.RankedAtoms.cut_positive line 302
  25. lemma OAI.Thomason.DirectedComplex.RankedAtoms.cut_add_complement line 311
  26. lemma OAI.Thomason.DirectedComplex.RankedAtoms.coefficient_derivative line 318
  27. lemma OAI.Thomason.DirectedComplex.RankedAtoms.derivative_nonneg_of_before line 325
  28. lemma OAI.Thomason.DirectedComplex.RankedAtoms.derivative_nonpos_of_after line 340
  29. lemma OAI.Thomason.DirectedComplex.RankedAtoms.cut_before_derivative line 355
  30. lemma OAI.Thomason.DirectedComplex.RankedAtoms.cut_after_derivative line 364
  31. lemma OAI.Thomason.DirectedComplex.RankedAtoms.rank_cut_positive line 373
  32. inductive OAI.Thomason.DirectedComplex.RankedAtoms.AtomPasting line 418
  33. lemma OAI.Thomason.DirectedComplex.RankedAtoms.common_atom_context line 423
  34. lemma OAI.Thomason.DirectedComplex.RankedAtoms.atom_context_pasting line 452
  35. theorem OAI.Thomason.DirectedComplex.RankedAtoms.atomic_pasting line 516
  36. theorem OAI.Thomason.DirectedComplex.RankedAtoms.all_atomic line 535
  37. instance OAI.Thomason.NormalizedChains.Prism.Word.finite line 553
  38. lemma OAI.Thomason.NormalizedChains.Prism.Word.empty_coefficient line 555
  39. lemma OAI.Thomason.NormalizedChains.Prism.Word.chain_ext line 561
  40. lemma OAI.Thomason.NormalizedChains.Prism.Word.chain_positive line 570
  41. def OAI.Thomason.NormalizedChains.Prism.Basis.indexEquiv line 584
  42. instance OAI.Thomason.NormalizedChains.Prism.Basis.finite line 594
  43. lemma OAI.Thomason.NormalizedChains.Prism.Basis.coefficient_homogeneous line 596
  44. lemma OAI.Thomason.NormalizedChains.Prism.Basis.coefficient_ext line 617
  45. lemma OAI.Thomason.NormalizedChains.Prism.Basis.positive_iff line 641
  46. def OAI.Thomason.NormalizedChains.Prism.Basis.rankedAtoms line 655
  47. theorem OAI.Thomason.NormalizedChains.Prism.Basis.cylinder_all_atomic line 669