OAI/Topology/ArtinGroups/ParabolicIntersections/RelativeUpperBasics.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Highest-incidence comparisons for upper edges of the relative filtration.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeSign_congr_above line 15
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeHeight_lt_iff line 30
  3. def OAI.HarmonicArtin.ParabolicIntersections.relativeIncidence line 46
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.relative_no_incidence line 49
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.relative_above_incidence line 60
  6. def OAI.HarmonicArtin.ParabolicIntersections.relativeUpperLevel line 65
  7. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeIncidence_le_upperLevel line 68
  8. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeProfile_eq_above_upper line 73
  9. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeBlock_eq_above_upper line 81