OAI/Topology/ArtinGroups/Geometry/ConvexWord.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicArtin.sourceConvexWord line 25
  2. lemma OAI.HarmonicArtin.sourceConvexWord_reduced line 29
  3. lemma OAI.HarmonicArtin.sourceConvexWord_reverse line 34
  4. def OAI.HarmonicArtin.sourceConvexVector line 41
  5. def OAI.HarmonicArtin.sourceConvexModel line 45
  6. lemma OAI.HarmonicArtin.sourceConvexModel_pure line 50
  7. lemma OAI.HarmonicArtin.sourceConvexModel_inclusion line 58
  8. lemma OAI.HarmonicArtin.sourceConvexModel_support line 65
  9. lemma OAI.HarmonicArtin.sourceConvexModel_counts line 70
  10. lemma OAI.HarmonicArtin.sourceConvexVector_support line 79
  11. lemma OAI.HarmonicArtin.sourceConvex_representative line 85
  12. theorem OAI.HarmonicArtin.source_convex_subobjects line 108
  13. theorem OAI.HarmonicArtin.source_convex_subobjects_interior line 128