Theorems · Theorem · order theory

CompositionSeries.Equivalent.snoc_snoc_swap

∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s : CompositionSeries X} {x₁ x₂ y₁ y₂ : X}
  {hsat₁ : JordanHolderLattice.IsMaximal (RelSeries.last s) x₁}
  {hsat₂ : JordanHolderLattice.IsMaximal (RelSeries.last s) x₂}
  {hsaty₁ : JordanHolderLattice.IsMaximal (RelSeries.snoc s x₁ hsat₁).last y₁}
  {hsaty₂ : JordanHolderLattice.IsMaximal (RelSeries.snoc s x₂ hsat₂).last y₂},
  JordanHolderLattice.Iso (RelSeries.last s, x₁) (x₂, y₂) →
    JordanHolderLattice.Iso (x₁, y₁) (RelSeries.last s, x₂) →
      CompositionSeries.Equivalent ((RelSeries.snoc s x₁ hsat₁).snoc y₁ hsaty₁)
        ((RelSeries.snoc s x₂ hsat₂).snoc y₂ hsaty₂)

Defined in

Mathlib.Order.JordanHolder

Cited by

1 results in Mathlib

Foundations

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

Assumes

LatticeJordanHolderLattice