OAI/Topology/ArtinGroups/ParabolicIntersections/RelativeLowerComparison.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Strict lower-neighbor comparisons for the relative height.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeMasks_ne_of_open_sign line 12
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeLower_ineligible_le line 24
  3. theorem OAI.HarmonicArtin.ParabolicIntersections.relativeLower_descending_has_eligible line 67

    Source documentation

    A descending lower face opens at least one eligible color.

    theorem relativeLower_descending_has_eligible {P Q:Deligne M} (h:Q<P)
    (he:relativeHeight M f U cutoff Q < relativeHeight M f U cutoff P) :
    ∃ i, RelativeEligible M f U cutoff P Q i := by
…

    Mentions: OAI.HarmonicArtin.Deligne, OAI.HarmonicArtin.ParabolicIntersections.relativeHeight, OAI.HarmonicArtin.ParabolicIntersections.RelativeEligible

  4. theorem OAI.HarmonicArtin.ParabolicIntersections.relativeLower_eligible_descending line 75

    Source documentation

    Opening only eligible colors strictly decreases height.

    theorem relativeLower_eligible_descending {P Q:Deligne M} (h:Q<P)
    (ha:∀i∈P.val.1,i∉Q.val.1→RelativeEligible M f U cutoff P Q i) :
    relativeHeight M f U cutoff Q < relativeHeight M f U cutoff P := by
…

    Mentions: OAI.HarmonicArtin.Deligne, OAI.HarmonicArtin.ParabolicIntersections.RelativeEligible, OAI.HarmonicArtin.ParabolicIntersections.relativeHeight