Theorems · Theorem · order theory

JordanHolderLattice.isMaximal_of_eq_inf

∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] (x b : X) {a y : X},
  x ⊓ y = a →
    x ≠ y → JordanHolderLattice.IsMaximal x b → JordanHolderLattice.IsMaximal y b → JordanHolderLattice.IsMaximal a y

Defined in: Mathlib.Order.JordanHolder
Cited by: 1 results in Mathlib
Foundations: Depth 9 from the axioms · uses propext
Assumes: Lattice JordanHolderLattice

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Latticestatement and proof · cited by 916
JordanHolderLatticestatement and proof · cited by 44
JordanHolderLattice.IsMaximalstatement and proof · cited by 42
JordanHolderLattice.sup_eq_of_isMaximalproof · cited by 2
JordanHolderLattice.isMaximal_inf_right_of_isMaximal_supproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

CompositionSeries.exists_last_eq_snoc_equivalentproof · cited by 1