OAI/Topology/ArtinGroups/ParabolicIntersections/ParabolicMinimal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Rank descent gives a minimal member of every nonempty family of parabolics.

  1. theorem OAI.HarmonicArtin.ParabolicIntersections.exists_minimal_parabolic line 13

    Source documentation

    A nonempty family of parabolic subgroups has an inclusion-minimal member. The argument follows the size of a displayed defining type and does not assume that rank is conjugacy invariant.

    theorem exists_minimal_parabolic (F : Set (Subgroup (Artin M))) (hF : F.Nonempty)
    (hpar : ∀ P∈F, IsParabolic M P) :
    ∃ P∈F, ∀ Q∈F, Q≤P → Q=P := by
…

    Mentions: OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.IsParabolic