OAI/Topology/ArtinGroups/ParabolicIntersections/RelativeEligible.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The eligible opened colors in a descending lower face.

  1. def OAI.HarmonicArtin.ParabolicIntersections.RelativeEligible line 12
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.relative_ineligible_top_ge line 19
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.relative_eligible_top_le line 37
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeSign_eq_at_lower_tie line 51
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.relative_ineligible_tie_sign line 61
  6. lemma OAI.HarmonicArtin.ParabolicIntersections.relative_eligible_tie_sign line 82
  7. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeEligible_positive line 92
  8. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeLowerLevel_prescribed_at_tie line 103