Theorems · Theorem · order theory

CompositionSeries.exists_last_eq_snoc_equivalent

∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] (s : CompositionSeries X) (x : X)
  (hm : JordanHolderLattice.IsMaximal x (RelSeries.last s)),
  RelSeries.head s ≤ x →
    ∃ t,
      RelSeries.head t = RelSeries.head s ∧
        t.length + 1 = s.length ∧ ∃ (htx : RelSeries.last t = x), s.Equivalent (RelSeries.snoc t (RelSeries.last s) ⋯)

Given a CompositionSeries, s, and an element x such that x is maximal inside s.last there is a series, t, such that t.last = x, t.head = s.head and snoc t s.last _ is equivalent to s.

Defined in

Mathlib.Order.JordanHolder

Cited by

1 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LatticeJordanHolderLattice