OAI/Topology/ArtinGroups/ParabolicIntersections/RelativeUpperConnected.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Connected descending upper neighborhoods, using their common active-color extension.

  1. def OAI.HarmonicArtin.ParabolicIntersections.relativeUpperTop line 13
  2. def OAI.HarmonicArtin.ParabolicIntersections.relativeUpperClip line 20
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.relative_le_upperClip line 26
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.relative_upperClip_le line 35
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.relative_upperClip_le_top line 41
  6. def OAI.HarmonicArtin.ParabolicIntersections.RelativeDescendingUpper line 47
  7. lemma OAI.HarmonicArtin.ParabolicIntersections.relative_upperClip_descending line 50
  8. lemma OAI.HarmonicArtin.ParabolicIntersections.relative_upperTop_descending line 65
  9. lemma OAI.HarmonicArtin.ParabolicIntersections.within_symm line 83
  10. theorem OAI.HarmonicArtin.ParabolicIntersections.relative_descending_upper_connected line 93

    Source documentation

    Descending upper neighbors are connected through descending upper neighbors.

    theorem relative_descending_upper_connected (P : RelativeVertex M Y x)
    (hYU : ∀ i ∈ Y, (.inl i : S ⊕ Unit) ∈ U)
    (R Q : RelativeVertex M Y x)
    (hR : RelativeDescendingUpper M f U cutoff Y x P R)
    (hQ : RelativeDescendingUpper M f U cutoff Y x P Q) :
    PathWithin (relativeAdjacent M) (RelativeDescendingUpper M f U cutoff Y x P) R Q := by
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.RelativeVertex, OAI.HarmonicArtin.ParabolicIntersections.RelativeDescendingUpper, OAI.HarmonicArtin.ParabolicIntersections.PathWithin, OAI.HarmonicArtin.ParabolicIntersections.relativeAdjacent