OAI/Topology/ArtinGroups/ParabolicIntersections/RelativeTieLower.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Transferring an eligible opening across a tied inclusion.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeProfiles_eq_of_tie line 14
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.relativePeak_eq_of_tie line 19
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeEligible_visible line 25
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeVisible_commutes line 32
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeEligible_single_open line 41
  6. theorem OAI.HarmonicArtin.ParabolicIntersections.relativeTie_lower_nonempty line 75

    Source documentation

    A descending lower neighbor at the larger end of a tie yields one at its smaller end. The invisible group factor is omitted from the representative.

    theorem relativeTie_lower_nonempty (Y:Set S) {P Q:Deligne M} (hPQ:P≤Q) (hQ:Q.val.1⊆Y)
    (htie:relativeHeight M f U cutoff P=relativeHeight M f U cutoff Q)
    (R:Deligne M) (hR:R<Q) (hdesc:relativeHeight M f U cutoff R<relativeHeight M f U cutoff Q) :
    ∃ V:Deligne M,V<P ∧ relativeHeight M f U cutoff V<relativeHeight M f U cutoff P := by
…

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