OAI/Topology/ArtinGroups/ParabolicIntersections/NoncommutingGraph.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Irreducibility is connectedness of the noncommutation graph.

  1. def OAI.HarmonicArtin.ParabolicIntersections.noncommutingGraph line 10
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.noncommuting_reachable line 17
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.list_first_outside line 27

    Source documentation

    A list with a term outside a set has an initial segment whose last term is the first outside term.

    lemma list_first_outside (C : Set S) (l : List S) (h : ∃ s∈l,s∉C) :
    ∃ u s v, l=u++s::v ∧ (∀ t∈u,t∈C) ∧ s∉C := by
…