RelativeLowerConnected.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Comparability paths in the descending lower neighborhood.

lemma OAI.HarmonicArtin.ParabolicIntersections.orderWeights_comparability_connected line 13
theorem OAI.HarmonicArtin.ParabolicIntersections.relativeDescendingLower_contractible line 37
def OAI.HarmonicArtin.ParabolicIntersections.RelativeStrictLower line 49
theorem OAI.HarmonicArtin.ParabolicIntersections.relative_descending_lower_connected line 53
Source documentation
Any two descending lower neighbors are joined within that same neighborhood.
```
theorem relative_descending_lower_connected {Y:Set S} {x:Artin M} (P:RelativeVertex M Y x)
    (hU:U⊆Set.range (Sum.inl:S→S⊕Unit)) (hf:(.inl f:S⊕Unit)∉U)
    (hxA:sourceCosetRepresentative M P.val∈artinParabolic M {f}ᶜ)
    (R Q:RelativeVertex M Y x)
    (hR:RelativeStrictLower M f U cutoff P R) (hQ:RelativeStrictLower M f U cutoff P Q) :
    PathWithin (relativeAdjacent M) (RelativeStrictLower M f U cutoff P) R Q := by
…
```
Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.RelativeVertex, OAI.HarmonicArtin.sourceCosetRepresentative, OAI.HarmonicArtin.artinParabolic, OAI.HarmonicArtin.ParabolicIntersections.RelativeStrictLower, OAI.HarmonicArtin.ParabolicIntersections.PathWithin, OAI.HarmonicArtin.ParabolicIntersections.relativeAdjacent