OAI/Topology/ArtinGroups/ParabolicIntersections/PositiveSupport.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Support of an element of the actual positive Artin monoid.

  1. structure OAI.HarmonicArtin.ParabolicIntersections.SupportValue line 10
  2. instance OAI.HarmonicArtin.ParabolicIntersections.(instance at line 13) line 13
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.supportValue_word line 21
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.altList_support line 29
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.support_relations line 40
  6. def OAI.HarmonicArtin.ParabolicIntersections.positiveSupportHom line 54
  7. def OAI.HarmonicArtin.ParabolicIntersections.positiveSupport line 57
  8. lemma OAI.HarmonicArtin.ParabolicIntersections.positiveSupport_one line 60
  9. lemma OAI.HarmonicArtin.ParabolicIntersections.positiveSupport_generator line 65
  10. lemma OAI.HarmonicArtin.ParabolicIntersections.positiveSupport_mul line 68
  11. lemma OAI.HarmonicArtin.ParabolicIntersections.positiveSupport_word line 74
  12. theorem OAI.HarmonicArtin.ParabolicIntersections.positiveSupport_word_exists line 86

    Source documentation

    Support inclusion gives a word using only the specified colors.

    theorem positiveSupport_word_exists (a : PositiveArtin M) (J : Set S)
    (ha : positiveSupport M a ⊆ J) :
    ∃ w : List S, wordPositive M w=a ∧ ∀ s ∈ w, s ∈ J := by
…

    Mentions: OAI.HarmonicArtin.PositiveArtin, OAI.HarmonicArtin.ParabolicIntersections.positiveSupport, OAI.HarmonicArtin.wordPositive