OAI/Topology/ArtinGroups/ParabolicIntersections/PointedCosetExteriorCap.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedCoset_exterior_cap line 21
2. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedCoset_exterior_multiplicity line 33
3. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedCosetVector_open_at line 43
4. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedResidue_exterior_cap line 49
5. lemma OAI.HarmonicArtin.ParabolicIntersections.pointedCoset_avoids_frame line 72

   Source documentation

   Frame avoidance persists throughout a coset whose type avoids the frame.

   lemma pointedCoset_avoids_frame (P : Deligne M) (x z : Artin M)
       (hx : x ∈ P.val.2) (hz : z ∈ P.val.2) (I : Set S)
       (hPI : P.val.1 ⊆ I) (hf : f ∉ I) (hxA : x ∈ artinParabolic M {f}ᶜ) :
       z ∈ artinParabolic M {f}ᶜ := by
   …

   Mentions: OAI.HarmonicArtin.Deligne, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.artinParabolic