OAI/Topology/ArtinGroups/ParabolicIntersections/RelativeLowerBasics.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The highest changed level on a lower edge, including invisible opened colors.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeLowerLevel_attained line 13
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeBlock_eq_above_lower line 48
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeHeight_eq_of_opened_zero line 75