OAI/Topology/ArtinGroups/ParabolicIntersections/RelativeUpperSigns.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Active-color rows and full sign masks at an upper comparison level.

  1. def OAI.HarmonicArtin.ParabolicIntersections.relativeColorActive line 12
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.relative_active_incident line 15
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.relative_active_sign line 25
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.relative_inactive_sign line 42
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.relative_upper_inactive_rows line 66
  6. lemma OAI.HarmonicArtin.ParabolicIntersections.relative_upper_active_rows line 77
  7. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeUpperLevel_incident line 91
  8. lemma OAI.HarmonicArtin.ParabolicIntersections.relative_sign_upper_tie line 120
  9. lemma OAI.HarmonicArtin.ParabolicIntersections.relative_mask_upper_nonneg line 131
  10. lemma OAI.HarmonicArtin.ParabolicIntersections.relative_mask_upper_nonpos line 150
  11. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeBlock_lt_of_mask line 169